Termination proof of /tmp/tmpRQv3u7/Power.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 710 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 210 ms)

        ↳7 IDP

        ↳8 IDPNonInfProof (⇒, 120 ms)

        ↳9 IDP

        ↳10 IDependencyGraphProof (⇔, 0 ms)

        ↳11 TRUE

    ↳12 JBCTerminationSCC

        ↳13 SCCToIDPv1Proof (⇒, 150 ms)

        ↳14 IDP

        ↳15 IDPNonInfProof (⇒, 100 ms)

        ↳16 IDP

        ↳17 IDependencyGraphProof (⇔, 0 ms)

        ↳18 TRUE

    ↳19 JBCTerminationSCC

        ↳20 SCCToIDPv1Proof (⇒, 1190 ms)

        ↳21 IDP

        ↳22 IDPNonInfProof (⇒, 120 ms)

        ↳23 AND

            ↳24 IDP

                ↳25 IDependencyGraphProof (⇔, 0 ms)

                ↳26 TRUE

            ↳27 IDP

                ↳28 IDependencyGraphProof (⇔, 0 ms)

                ↳29 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Apple Inc.) Main-Class: Power

public class Power {
    public static void main(String args[]) {
	for (int i = 0; i < args.length; i++) {
	    even(power(args.length, args[i].length()));
	    odd( power(args.length, args[i].length()));
	}
	// power(args.length, args.length);
    }

    public static int power(int a, int n) {
	if (n <= 0) return 1;
	else if (n == 1) return a;
	else {
	    int r = power(a * a, n/2);
	    if (n % 2 == 0) return r;
	    else return a * r;
	}
    }

    public static boolean even(int n) {
	if (n <= 0) return true;
	else if (n == 1) return false;
	else return odd(n - 1);
    }

    public static boolean odd(int n) {
	if (n <= 0) return false;
	else if (n == 1) return true;
	else return even(n - 1);
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Power.main([Ljava/lang/String;)V: Graph of 194 nodes with 1 SCC.

Power.power(II)I: Graph of 46 nodes with 0 SCCs.

Power.even(I)Z: Graph of 28 nodes with 0 SCCs.

Power.odd(I)Z: Graph of 26 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 3 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Power.even(I)Z, Power.odd(I)Z
SCC calls the following helper methods: Power.even(I)Z, Power.odd(I)Z
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 26 rules for P and 24 rules for R.

P rules:
1081_0_even_GT(EOS(STATIC_1081), i286, i286) → 1090_0_even_GT(EOS(STATIC_1090), i286, i286)
1090_0_even_GT(EOS(STATIC_1090), i286, i286) → 1098_0_even_Load(EOS(STATIC_1098), i286) | >(i286, 0)
1098_0_even_Load(EOS(STATIC_1098), i286) → 1105_0_even_ConstantStackPush(EOS(STATIC_1105), i286, i286)
1105_0_even_ConstantStackPush(EOS(STATIC_1105), i286, i286) → 1114_0_even_NE(EOS(STATIC_1114), i286, i286, 1)
1114_0_even_NE(EOS(STATIC_1114), i288, i288, matching1) → 1126_0_even_NE(EOS(STATIC_1126), i288, i288, 1) | =(matching1, 1)
1126_0_even_NE(EOS(STATIC_1126), i288, i288, matching1) → 1142_0_even_Load(EOS(STATIC_1142), i288) | &&(!(=(i288, 1)), =(matching1, 1))
1142_0_even_Load(EOS(STATIC_1142), i288) → 1152_0_even_ConstantStackPush(EOS(STATIC_1152), i288)
1152_0_even_ConstantStackPush(EOS(STATIC_1152), i288) → 1165_0_even_IntArithmetic(EOS(STATIC_1165), i288, 1)
1165_0_even_IntArithmetic(EOS(STATIC_1165), i288, matching1) → 1186_0_even_InvokeMethod(EOS(STATIC_1186), -(i288, 1)) | &&(>(i288, 0), =(matching1, 1))
1186_0_even_InvokeMethod(EOS(STATIC_1186), i306) → 1206_1_even_InvokeMethod(1206_0_odd_Load(EOS(STATIC_1206), i306), i306)
1206_0_odd_Load(EOS(STATIC_1206), i306) → 1216_0_odd_Load(EOS(STATIC_1216), i306)
1216_0_odd_Load(EOS(STATIC_1216), i306) → 1516_0_odd_Load(EOS(STATIC_1516), i306)
1516_0_odd_Load(EOS(STATIC_1516), i450) → 1525_0_odd_GT(EOS(STATIC_1525), i450, i450)
1525_0_odd_GT(EOS(STATIC_1525), i468, i468) → 1542_0_odd_GT(EOS(STATIC_1542), i468, i468)
1542_0_odd_GT(EOS(STATIC_1542), i468, i468) → 1552_0_odd_Load(EOS(STATIC_1552), i468) | >(i468, 0)
1552_0_odd_Load(EOS(STATIC_1552), i468) → 1563_0_odd_ConstantStackPush(EOS(STATIC_1563), i468, i468)
1563_0_odd_ConstantStackPush(EOS(STATIC_1563), i468, i468) → 1574_0_odd_NE(EOS(STATIC_1574), i468, i468, 1)
1574_0_odd_NE(EOS(STATIC_1574), i488, i488, matching1) → 1585_0_odd_NE(EOS(STATIC_1585), i488, i488, 1) | =(matching1, 1)
1585_0_odd_NE(EOS(STATIC_1585), i488, i488, matching1) → 1597_0_odd_Load(EOS(STATIC_1597), i488) | &&(!(=(i488, 1)), =(matching1, 1))
1597_0_odd_Load(EOS(STATIC_1597), i488) → 1605_0_odd_ConstantStackPush(EOS(STATIC_1605), i488)
1605_0_odd_ConstantStackPush(EOS(STATIC_1605), i488) → 1613_0_odd_IntArithmetic(EOS(STATIC_1613), i488, 1)
1613_0_odd_IntArithmetic(EOS(STATIC_1613), i488, matching1) → 1624_0_odd_InvokeMethod(EOS(STATIC_1624), -(i488, 1)) | &&(>(i488, 0), =(matching1, 1))
1624_0_odd_InvokeMethod(EOS(STATIC_1624), i497) → 1640_1_odd_InvokeMethod(1640_0_even_Load(EOS(STATIC_1640), i497), i497)
1640_0_even_Load(EOS(STATIC_1640), i497) → 1643_0_even_Load(EOS(STATIC_1643), i497)
1643_0_even_Load(EOS(STATIC_1643), i497) → 1075_0_even_Load(EOS(STATIC_1075), i497)
1075_0_even_Load(EOS(STATIC_1075), i278) → 1081_0_even_GT(EOS(STATIC_1081), i278, i278)
R rules:
1081_0_even_GT(EOS(STATIC_1081), matching1, matching2) → 1089_0_even_GT(EOS(STATIC_1089), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
1089_0_even_GT(EOS(STATIC_1089), matching1, matching2) → 1096_0_even_ConstantStackPush(EOS(STATIC_1096), 0) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
1096_0_even_ConstantStackPush(EOS(STATIC_1096), matching1) → 1104_0_even_Return(EOS(STATIC_1104), 0) | =(matching1, 0)
1114_0_even_NE(EOS(STATIC_1114), matching1, matching2, matching3) → 1125_0_even_NE(EOS(STATIC_1125), 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
1125_0_even_NE(EOS(STATIC_1125), matching1, matching2, matching3) → 1140_0_even_ConstantStackPush(EOS(STATIC_1140), 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
1140_0_even_ConstantStackPush(EOS(STATIC_1140), matching1) → 1151_0_even_Return(EOS(STATIC_1151), 1, 0) | =(matching1, 1)
1206_1_even_InvokeMethod(1604_0_odd_Return(EOS(STATIC_1604), matching1, matching2), matching3) → 1638_0_odd_Return(EOS(STATIC_1638), 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
1206_1_even_InvokeMethod(1665_0_odd_Return(EOS(STATIC_1665), i337), i513) → 1679_0_odd_Return(EOS(STATIC_1679), i513, i337)
1261_0_odd_Return(EOS(STATIC_1261), matching1, matching2, matching3) → 1273_0_even_Return(EOS(STATIC_1273), 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
1267_0_odd_Return(EOS(STATIC_1267), i338, i337) → 1276_0_even_Return(EOS(STATIC_1276), i337)
1273_0_even_Return(EOS(STATIC_1273), matching1) → 1276_0_even_Return(EOS(STATIC_1276), 1) | =(matching1, 1)
1638_0_odd_Return(EOS(STATIC_1638), matching1, matching2, matching3) → 1261_0_odd_Return(EOS(STATIC_1261), 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
1679_0_odd_Return(EOS(STATIC_1679), i513, i337) → 1267_0_odd_Return(EOS(STATIC_1267), i513, i337)
1525_0_odd_GT(EOS(STATIC_1525), matching1, matching2) → 1541_0_odd_GT(EOS(STATIC_1541), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
1541_0_odd_GT(EOS(STATIC_1541), matching1, matching2) → 1551_0_odd_ConstantStackPush(EOS(STATIC_1551), 0) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
1551_0_odd_ConstantStackPush(EOS(STATIC_1551), matching1) → 1561_0_odd_Return(EOS(STATIC_1561), 0, 0) | =(matching1, 0)
1574_0_odd_NE(EOS(STATIC_1574), matching1, matching2, matching3) → 1584_0_odd_NE(EOS(STATIC_1584), 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
1584_0_odd_NE(EOS(STATIC_1584), matching1, matching2, matching3) → 1596_0_odd_ConstantStackPush(EOS(STATIC_1596), 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
1596_0_odd_ConstantStackPush(EOS(STATIC_1596), matching1) → 1604_0_odd_Return(EOS(STATIC_1604), 1, 1) | =(matching1, 1)
1640_1_odd_InvokeMethod(1151_0_even_Return(EOS(STATIC_1151), matching1, matching2), matching3) → 1656_0_even_Return(EOS(STATIC_1656), 1, 1, 0) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 1))
1640_1_odd_InvokeMethod(1276_0_even_Return(EOS(STATIC_1276), i337), i505) → 1657_0_even_Return(EOS(STATIC_1657), i505, i337)
1656_0_even_Return(EOS(STATIC_1656), matching1, matching2, matching3) → 1662_0_odd_Return(EOS(STATIC_1662), 0) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 0))
1657_0_even_Return(EOS(STATIC_1657), i505, i337) → 1665_0_odd_Return(EOS(STATIC_1665), i337)
1662_0_odd_Return(EOS(STATIC_1662), matching1) → 1665_0_odd_Return(EOS(STATIC_1665), 0) | =(matching1, 0)

Combined rules. Obtained 1 conditional rules for P and 5 conditional rules for R.

P rules:
1081_0_even_GT(EOS(STATIC_1081), x0, x0) → 1206_1_even_InvokeMethod(1640_1_odd_InvokeMethod(1081_0_even_GT(EOS(STATIC_1081), -(-(x0, 1), 1), -(-(x0, 1), 1)), -(-(x0, 1), 1)), -(x0, 1)) | &&(>(x0, 1), !(=(-(x0, 1), 1)))
R rules:
1081_0_even_GT(EOS(STATIC_1081), 0, 0) → 1104_0_even_Return(EOS(STATIC_1104), 0)
1206_1_even_InvokeMethod(1604_0_odd_Return(EOS(STATIC_1604), 1, 1), 1) → 1276_0_even_Return(EOS(STATIC_1276), 1)
1206_1_even_InvokeMethod(1665_0_odd_Return(EOS(STATIC_1665), x0), x1) → 1276_0_even_Return(EOS(STATIC_1276), x0)
1640_1_odd_InvokeMethod(1276_0_even_Return(EOS(STATIC_1276), x0), x1) → 1665_0_odd_Return(EOS(STATIC_1665), x0)
1640_1_odd_InvokeMethod(1151_0_even_Return(EOS(STATIC_1151), 1, 0), 1) → 1665_0_odd_Return(EOS(STATIC_1665), 0)

Filtered ground terms:

1081_0_even_GT(x1, x2, x3) → 1081_0_even_GT(x2, x3)
Cond_1081_0_even_GT(x1, x2, x3, x4) → Cond_1081_0_even_GT(x1, x3, x4)
1665_0_odd_Return(x1, x2) → 1665_0_odd_Return(x2)
1151_0_even_Return(x1, x2, x3) → 1151_0_even_Return
1276_0_even_Return(x1, x2) → 1276_0_even_Return(x2)
1604_0_odd_Return(x1, x2, x3) → 1604_0_odd_Return
1104_0_even_Return(x1, x2) → 1104_0_even_Return

Filtered duplicate args:

1081_0_even_GT(x1, x2) → 1081_0_even_GT(x2)
Cond_1081_0_even_GT(x1, x2, x3) → Cond_1081_0_even_GT(x1, x3)

Combined rules. Obtained 1 conditional rules for P and 5 conditional rules for R.

P rules:
1081_0_even_GT(x0) → 1206_1_even_InvokeMethod(1640_1_odd_InvokeMethod(1081_0_even_GT(-(-(x0, 1), 1)), -(-(x0, 1), 1)), -(x0, 1)) | &&(>(x0, 1), !(=(-(x0, 1), 1)))
R rules:
1081_0_even_GT(0) → 1104_0_even_Return
1206_1_even_InvokeMethod(1604_0_odd_Return, 1) → 1276_0_even_Return(1)
1206_1_even_InvokeMethod(1665_0_odd_Return(x0), x1) → 1276_0_even_Return(x0)
1640_1_odd_InvokeMethod(1276_0_even_Return(x0), x1) → 1665_0_odd_Return(x0)
1640_1_odd_InvokeMethod(1151_0_even_Return, 1) → 1665_0_odd_Return(0)

Performed bisimulation on rules. Used the following equivalence classes: {[1104_0_even_Return, 1604_0_odd_Return, 1151_0_even_Return]=1104_0_even_Return}

Finished conversion. Obtained 2 rules for P and 5 rules for R. System has predefined symbols.

P rules:
1081_0_EVEN_GT(x0) → COND_1081_0_EVEN_GT(&&(>(x0, 1), !(=(-(x0, 1), 1))), x0)
COND_1081_0_EVEN_GT(TRUE, x0) → 1081_0_EVEN_GT(-(-(x0, 1), 1))
R rules:
1081_0_even_GT(0) → 1104_0_even_Return
1206_1_even_InvokeMethod(1104_0_even_Return, 1) → 1276_0_even_Return(1)
1206_1_even_InvokeMethod(1665_0_odd_Return(x0), x1) → 1276_0_even_Return(x0)
1640_1_odd_InvokeMethod(1276_0_even_Return(x0), x1) → 1665_0_odd_Return(x0)
1640_1_odd_InvokeMethod(1104_0_even_Return, 1) → 1665_0_odd_Return(0)

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

The ITRS R consists of the following rules:
1081_0_even_GT(0) → 1104_0_even_Return
1206_1_even_InvokeMethod(1104_0_even_Return, 1) → 1276_0_even_Return(1)
1206_1_even_InvokeMethod(1665_0_odd_Return(x0), x1) → 1276_0_even_Return(x0)
1640_1_odd_InvokeMethod(1276_0_even_Return(x0), x1) → 1665_0_odd_Return(x0)
1640_1_odd_InvokeMethod(1104_0_even_Return, 1) → 1665_0_odd_Return(0)

The integer pair graph contains the following rules and edges:
(0): 1081_0_EVEN_GT(x0[0]) → COND_1081_0_EVEN_GT(x0[0] > 1 && !(x0[0] - 1 = 1), x0[0])
(1): COND_1081_0_EVEN_GT(TRUE, x0[1]) → 1081_0_EVEN_GT(x0[1] - 1 - 1)

(0) -> (1), if (x0[0] > 1 && !(x0[0] - 1 = 1) ∧x0[0] →^* x0[1])

(1) -> (0), if (x0[1] - 1 - 1 →^* x0[0])

The set Q consists of the following terms:
1081_0_even_GT(0)
1206_1_even_InvokeMethod(1104_0_even_Return, 1)
1206_1_even_InvokeMethod(1665_0_odd_Return(x0), x1)
1640_1_odd_InvokeMethod(1276_0_even_Return(x0), x1)
1640_1_odd_InvokeMethod(1104_0_even_Return, 1)

(8) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@4468dbbe Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 1081_0_EVEN_GT(x0) → COND_1081_0_EVEN_GT(&&(>(x0, 1), !(=(-(x0, 1), 1))), x0) the following chains were created:

We consider the chain 1081_0_EVEN_GT(x0[0]) → COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0]), COND_1081_0_EVEN_GT(TRUE, x0[1]) → 1081_0_EVEN_GT(-(-(x0[1], 1), 1)) which results in the following constraint:
(1)    (&&(>(x0[0], 1), !(=(-(x0[0], 1), 1)))=TRUE∧x0[0]=x0[1] ⇒ 1081_0_EVEN_GT(x0[0])≥NonInfC∧1081_0_EVEN_GT(x0[0])≥COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])∧(U^Increasing(COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])), ≥))

We simplified constraint (1) using rules (IV), (IDP_BOOLEAN) which results in the following new constraints:
(2)    (>(x0[0], 1)=TRUE∧<(-(x0[0], 1), 1)=TRUE ⇒ 1081_0_EVEN_GT(x0[0])≥NonInfC∧1081_0_EVEN_GT(x0[0])≥COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])∧(U^Increasing(COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])), ≥))

(3)    (>(x0[0], 1)=TRUE∧>(-(x0[0], 1), 1)=TRUE ⇒ 1081_0_EVEN_GT(x0[0])≥NonInfC∧1081_0_EVEN_GT(x0[0])≥COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])∧(U^Increasing(COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(4)    (x0[0] + [-2] ≥ 0∧[1] + [-1]x0[0] ≥ 0 ⇒ (U^Increasing(COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_17 + (-1)Bound*bni_17] + [(2)bni_17]x0[0] ≥ 0∧[1 + (-1)bso_18] ≥ 0)

We simplified constraint (3) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(5)    (x0[0] + [-2] ≥ 0∧x0[0] + [-3] ≥ 0 ⇒ (U^Increasing(COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_17 + (-1)Bound*bni_17] + [(2)bni_17]x0[0] ≥ 0∧[1 + (-1)bso_18] ≥ 0)

We simplified constraint (4) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(6)    (x0[0] + [-2] ≥ 0∧[1] + [-1]x0[0] ≥ 0 ⇒ (U^Increasing(COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_17 + (-1)Bound*bni_17] + [(2)bni_17]x0[0] ≥ 0∧[1 + (-1)bso_18] ≥ 0)

We simplified constraint (5) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(7)    (x0[0] + [-2] ≥ 0∧x0[0] + [-3] ≥ 0 ⇒ (U^Increasing(COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_17 + (-1)Bound*bni_17] + [(2)bni_17]x0[0] ≥ 0∧[1 + (-1)bso_18] ≥ 0)

We simplified constraint (6) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(8)    (x0[0] + [-2] ≥ 0∧[1] + [-1]x0[0] ≥ 0 ⇒ (U^Increasing(COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_17 + (-1)Bound*bni_17] + [(2)bni_17]x0[0] ≥ 0∧[1 + (-1)bso_18] ≥ 0)

We simplified constraint (7) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(9)    (x0[0] + [-2] ≥ 0∧x0[0] + [-3] ≥ 0 ⇒ (U^Increasing(COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_17 + (-1)Bound*bni_17] + [(2)bni_17]x0[0] ≥ 0∧[1 + (-1)bso_18] ≥ 0)

We solved constraint (8) using rule (IDP_SMT_SPLIT).We simplified constraint (9) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(10)    (x0[0] ≥ 0∧[-1] + x0[0] ≥ 0 ⇒ (U^Increasing(COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[(5)bni_17 + (-1)Bound*bni_17] + [(2)bni_17]x0[0] ≥ 0∧[1 + (-1)bso_18] ≥ 0)

We simplified constraint (10) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(11)    ([1] + x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[(7)bni_17 + (-1)Bound*bni_17] + [(2)bni_17]x0[0] ≥ 0∧[1 + (-1)bso_18] ≥ 0)

For Pair COND_1081_0_EVEN_GT(TRUE, x0) → 1081_0_EVEN_GT(-(-(x0, 1), 1)) the following chains were created:

We consider the chain COND_1081_0_EVEN_GT(TRUE, x0[1]) → 1081_0_EVEN_GT(-(-(x0[1], 1), 1)) which results in the following constraint:
(12)    (COND_1081_0_EVEN_GT(TRUE, x0[1])≥NonInfC∧COND_1081_0_EVEN_GT(TRUE, x0[1])≥1081_0_EVEN_GT(-(-(x0[1], 1), 1))∧(U^Increasing(1081_0_EVEN_GT(-(-(x0[1], 1), 1))), ≥))

We simplified constraint (12) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(13)    ((U^Increasing(1081_0_EVEN_GT(-(-(x0[1], 1), 1))), ≥)∧[bni_19] = 0∧[3 + (-1)bso_20] ≥ 0)

We simplified constraint (13) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(14)    ((U^Increasing(1081_0_EVEN_GT(-(-(x0[1], 1), 1))), ≥)∧[bni_19] = 0∧[3 + (-1)bso_20] ≥ 0)

We simplified constraint (14) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(15)    ((U^Increasing(1081_0_EVEN_GT(-(-(x0[1], 1), 1))), ≥)∧[bni_19] = 0∧[3 + (-1)bso_20] ≥ 0)

We simplified constraint (15) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(16)    ((U^Increasing(1081_0_EVEN_GT(-(-(x0[1], 1), 1))), ≥)∧[bni_19] = 0∧0 = 0∧[3 + (-1)bso_20] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

1081_0_EVEN_GT(x0) → COND_1081_0_EVEN_GT(&&(>(x0, 1), !(=(-(x0, 1), 1))), x0)
- ([1] + x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[(7)bni_17 + (-1)Bound*bni_17] + [(2)bni_17]x0[0] ≥ 0∧[1 + (-1)bso_18] ≥ 0)
COND_1081_0_EVEN_GT(TRUE, x0) → 1081_0_EVEN_GT(-(-(x0, 1), 1))
- ((U^Increasing(1081_0_EVEN_GT(-(-(x0[1], 1), 1))), ≥)∧[bni_19] = 0∧0 = 0∧[3 + (-1)bso_20] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(1081_0_even_GT(x₁)) = [-1]
POL(0) = 0
POL(1104_0_even_Return) = [-1]
POL(1206_1_even_InvokeMethod(x₁, x₂)) = [-1]
POL(1) = [1]
POL(1276_0_even_Return(x₁)) = [-1]
POL(1665_0_odd_Return(x₁)) = [-1]
POL(1640_1_odd_InvokeMethod(x₁, x₂)) = [-1]
POL(1081_0_EVEN_GT(x₁)) = [1] + [2]x₁
POL(COND_1081_0_EVEN_GT(x₁, x₂)) = [2]x₂
POL(&&(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(!(x₁)) = [-1]
POL(=(x₁, x₂)) = [-1]
POL(-(x₁, x₂)) = x₁ + [-1]x₂

The following pairs are in P_>:

1081_0_EVEN_GT(x0[0]) → COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])
COND_1081_0_EVEN_GT(TRUE, x0[1]) → 1081_0_EVEN_GT(-(-(x0[1], 1), 1))

The following pairs are in P_bound:

1081_0_EVEN_GT(x0[0]) → COND_1081_0_EVEN_GT(&&(>(x0[0], 1), !(=(-(x0[0], 1), 1))), x0[0])

The following pairs are in P_≥:
none

There are no usable rules.

(9) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
1081_0_even_GT(0) → 1104_0_even_Return
1206_1_even_InvokeMethod(1104_0_even_Return, 1) → 1276_0_even_Return(1)
1206_1_even_InvokeMethod(1665_0_odd_Return(x0), x1) → 1276_0_even_Return(x0)
1640_1_odd_InvokeMethod(1276_0_even_Return(x0), x1) → 1665_0_odd_Return(x0)
1640_1_odd_InvokeMethod(1104_0_even_Return, 1) → 1665_0_odd_Return(0)

The integer pair graph contains the following rules and edges:
(1): COND_1081_0_EVEN_GT(TRUE, x0[1]) → 1081_0_EVEN_GT(x0[1] - 1 - 1)

The set Q consists of the following terms:
1081_0_even_GT(0)
1206_1_even_InvokeMethod(1104_0_even_Return, 1)
1206_1_even_InvokeMethod(1665_0_odd_Return(x0), x1)
1640_1_odd_InvokeMethod(1276_0_even_Return(x0), x1)
1640_1_odd_InvokeMethod(1104_0_even_Return, 1)

(10) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(11) TRUE

(12) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Power.power(II)I
SCC calls the following helper methods: Power.power(II)I
Performed SCC analyses: UsedFieldsAnalysis

(13) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 16 rules for P and 28 rules for R.

P rules:
932_0_power_GT(EOS(STATIC_932), i259, i259) → 939_0_power_GT(EOS(STATIC_939), i259, i259)
939_0_power_GT(EOS(STATIC_939), i259, i259) → 942_0_power_Load(EOS(STATIC_942), i259) | >(i259, 0)
942_0_power_Load(EOS(STATIC_942), i259) → 950_0_power_ConstantStackPush(EOS(STATIC_950), i259, i259)
950_0_power_ConstantStackPush(EOS(STATIC_950), i259, i259) → 959_0_power_NE(EOS(STATIC_959), i259, i259, 1)
959_0_power_NE(EOS(STATIC_959), i263, i263, matching1) → 970_0_power_NE(EOS(STATIC_970), i263, i263, 1) | =(matching1, 1)
970_0_power_NE(EOS(STATIC_970), i263, i263, matching1) → 979_0_power_Load(EOS(STATIC_979), i263) | &&(!(=(i263, 1)), =(matching1, 1))
979_0_power_Load(EOS(STATIC_979), i263) → 992_0_power_Load(EOS(STATIC_992), i263)
992_0_power_Load(EOS(STATIC_992), i263) → 1002_0_power_IntArithmetic(EOS(STATIC_1002), i263)
1002_0_power_IntArithmetic(EOS(STATIC_1002), i263) → 1013_0_power_Load(EOS(STATIC_1013), i263)
1013_0_power_Load(EOS(STATIC_1013), i263) → 1021_0_power_ConstantStackPush(EOS(STATIC_1021), i263, i263)
1021_0_power_ConstantStackPush(EOS(STATIC_1021), i263, i263) → 1035_0_power_IntArithmetic(EOS(STATIC_1035), i263, i263, 2)
1035_0_power_IntArithmetic(EOS(STATIC_1035), i263, i263, matching1) → 1046_0_power_InvokeMethod(EOS(STATIC_1046), i263, /(i263, 2)) | &&(>(i263, 1), =(matching1, 2))
1046_0_power_InvokeMethod(EOS(STATIC_1046), i263, i276) → 1055_1_power_InvokeMethod(1055_0_power_Load(EOS(STATIC_1055), i276), i263, i276)
1055_0_power_Load(EOS(STATIC_1055), i276) → 1064_0_power_Load(EOS(STATIC_1064), i276)
1064_0_power_Load(EOS(STATIC_1064), i276) → 926_0_power_Load(EOS(STATIC_926), i276)
926_0_power_Load(EOS(STATIC_926), i247) → 932_0_power_GT(EOS(STATIC_932), i247, i247)
R rules:
932_0_power_GT(EOS(STATIC_932), matching1, matching2) → 937_0_power_GT(EOS(STATIC_937), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
937_0_power_GT(EOS(STATIC_937), matching1, matching2) → 941_0_power_ConstantStackPush(EOS(STATIC_941), 0) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
941_0_power_ConstantStackPush(EOS(STATIC_941), matching1) → 949_0_power_Return(EOS(STATIC_949), 0) | =(matching1, 0)
959_0_power_NE(EOS(STATIC_959), matching1, matching2, matching3) → 969_0_power_NE(EOS(STATIC_969), 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
969_0_power_NE(EOS(STATIC_969), matching1, matching2, matching3) → 978_0_power_Load(EOS(STATIC_978), 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
978_0_power_Load(EOS(STATIC_978), matching1) → 991_0_power_Return(EOS(STATIC_991), 1) | =(matching1, 1)
1055_1_power_InvokeMethod(991_0_power_Return(EOS(STATIC_991), matching1), i263, matching2) → 1093_0_power_Return(EOS(STATIC_1093), i263, 1, 1) | &&(=(matching1, 1), =(matching2, 1))
1055_1_power_InvokeMethod(1328_0_power_Return(EOS(STATIC_1328)), i263, i369) → 1355_0_power_Return(EOS(STATIC_1355), i263, i369)
1055_1_power_InvokeMethod(1338_0_power_Return(EOS(STATIC_1338)), i263, i381) → 1373_0_power_Return(EOS(STATIC_1373), i263, i381)
1093_0_power_Return(EOS(STATIC_1093), i263, matching1, matching2) → 1100_0_power_Store(EOS(STATIC_1100), i263) | &&(=(matching1, 1), =(matching2, 1))
1100_0_power_Store(EOS(STATIC_1100), i263) → 1259_0_power_Store(EOS(STATIC_1259), i263)
1235_0_power_Return(EOS(STATIC_1235), i263, i316) → 1259_0_power_Store(EOS(STATIC_1259), i263)
1259_0_power_Store(EOS(STATIC_1259), i263) → 1282_0_power_Store(EOS(STATIC_1282), i263)
1269_0_power_Return(EOS(STATIC_1269), i263, i330) → 1282_0_power_Store(EOS(STATIC_1282), i263)
1282_0_power_Store(EOS(STATIC_1282), i263) → 1287_0_power_Load(EOS(STATIC_1287), i263)
1287_0_power_Load(EOS(STATIC_1287), i263) → 1292_0_power_ConstantStackPush(EOS(STATIC_1292), i263)
1292_0_power_ConstantStackPush(EOS(STATIC_1292), i263) → 1295_0_power_IntArithmetic(EOS(STATIC_1295), i263, 2)
1295_0_power_IntArithmetic(EOS(STATIC_1295), i263, matching1) → 1302_0_power_NE(EOS(STATIC_1302), %(i263, 2)) | =(matching1, 2)
1302_0_power_NE(EOS(STATIC_1302), matching1) → 1307_0_power_NE(EOS(STATIC_1307), 1) | =(matching1, 1)
1302_0_power_NE(EOS(STATIC_1302), matching1) → 1308_0_power_NE(EOS(STATIC_1308), 0) | =(matching1, 0)
1307_0_power_NE(EOS(STATIC_1307), matching1) → 1320_0_power_Load(EOS(STATIC_1320)) | &&(>(1, 0), =(matching1, 1))
1308_0_power_NE(EOS(STATIC_1308), matching1) → 1321_0_power_Load(EOS(STATIC_1321)) | =(matching1, 0)
1320_0_power_Load(EOS(STATIC_1320)) → 1327_0_power_Load(EOS(STATIC_1327))
1321_0_power_Load(EOS(STATIC_1321)) → 1328_0_power_Return(EOS(STATIC_1328))
1327_0_power_Load(EOS(STATIC_1327)) → 1332_0_power_IntArithmetic(EOS(STATIC_1332))
1332_0_power_IntArithmetic(EOS(STATIC_1332)) → 1338_0_power_Return(EOS(STATIC_1338))
1355_0_power_Return(EOS(STATIC_1355), i263, i369) → 1235_0_power_Return(EOS(STATIC_1235), i263, i369)
1373_0_power_Return(EOS(STATIC_1373), i263, i381) → 1269_0_power_Return(EOS(STATIC_1269), i263, i381)

Combined rules. Obtained 1 conditional rules for P and 6 conditional rules for R.

P rules:
932_0_power_GT(EOS(STATIC_932), x0, x0) → 1055_1_power_InvokeMethod(932_0_power_GT(EOS(STATIC_932), /(x0, 2), /(x0, 2)), x0, /(x0, 2)) | >(x0, 1)
R rules:
932_0_power_GT(EOS(STATIC_932), 0, 0) → 949_0_power_Return(EOS(STATIC_949), 0)
1055_1_power_InvokeMethod(991_0_power_Return(EOS(STATIC_991), 1), x1, 1) → 1302_0_power_NE(EOS(STATIC_1302), %(x1, 2))
1302_0_power_NE(EOS(STATIC_1302), 0) → 1328_0_power_Return(EOS(STATIC_1328))
1302_0_power_NE(EOS(STATIC_1302), 1) → 1338_0_power_Return(EOS(STATIC_1338))
1055_1_power_InvokeMethod(1328_0_power_Return(EOS(STATIC_1328)), x0, x1) → 1302_0_power_NE(EOS(STATIC_1302), %(x0, 2))
1055_1_power_InvokeMethod(1338_0_power_Return(EOS(STATIC_1338)), x0, x1) → 1302_0_power_NE(EOS(STATIC_1302), %(x0, 2))

Filtered ground terms:

932_0_power_GT(x1, x2, x3) → 932_0_power_GT(x2, x3)
Cond_932_0_power_GT(x1, x2, x3, x4) → Cond_932_0_power_GT(x1, x3, x4)
1302_0_power_NE(x1, x2) → 1302_0_power_NE(x2)
1338_0_power_Return(x1) → 1338_0_power_Return
1328_0_power_Return(x1) → 1328_0_power_Return
991_0_power_Return(x1, x2) → 991_0_power_Return
949_0_power_Return(x1, x2) → 949_0_power_Return

Filtered duplicate args:

932_0_power_GT(x1, x2) → 932_0_power_GT(x2)
Cond_932_0_power_GT(x1, x2, x3) → Cond_932_0_power_GT(x1, x3)

Combined rules. Obtained 1 conditional rules for P and 6 conditional rules for R.

P rules:
932_0_power_GT(x0) → 1055_1_power_InvokeMethod(932_0_power_GT(/(x0, 2)), x0, /(x0, 2)) | >(x0, 1)
R rules:
932_0_power_GT(0) → 949_0_power_Return
1055_1_power_InvokeMethod(991_0_power_Return, x1, 1) → 1302_0_power_NE(%(x1, 2))
1302_0_power_NE(0) → 1328_0_power_Return
1302_0_power_NE(1) → 1338_0_power_Return
1055_1_power_InvokeMethod(1328_0_power_Return, x0, x1) → 1302_0_power_NE(%(x0, 2))
1055_1_power_InvokeMethod(1338_0_power_Return, x0, x1) → 1302_0_power_NE(%(x0, 2))

Performed bisimulation on rules. Used the following equivalence classes: {[949_0_power_Return, 991_0_power_Return, 1328_0_power_Return, 1338_0_power_Return]=949_0_power_Return}

Finished conversion. Obtained 2 rules for P and 5 rules for R. System has predefined symbols.

P rules:
932_0_POWER_GT(x0) → COND_932_0_POWER_GT(>(x0, 1), x0)
COND_932_0_POWER_GT(TRUE, x0) → 932_0_POWER_GT(/(x0, 2))
R rules:
932_0_power_GT(0) → 949_0_power_Return
1055_1_power_InvokeMethod(949_0_power_Return, x1, 1) → 1302_0_power_NE(%(x1, 2))
1302_0_power_NE(0) → 949_0_power_Return
1302_0_power_NE(1) → 949_0_power_Return
1055_1_power_InvokeMethod(949_0_power_Return, x0, x1) → 1302_0_power_NE(%(x0, 2))

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
932_0_power_GT(0) → 949_0_power_Return
1055_1_power_InvokeMethod(949_0_power_Return, x1, 1) → 1302_0_power_NE(x1 % 2)
1302_0_power_NE(0) → 949_0_power_Return
1302_0_power_NE(1) → 949_0_power_Return
1055_1_power_InvokeMethod(949_0_power_Return, x0, x1) → 1302_0_power_NE(x0 % 2)

The integer pair graph contains the following rules and edges:
(0): 932_0_POWER_GT(x0[0]) → COND_932_0_POWER_GT(x0[0] > 1, x0[0])
(1): COND_932_0_POWER_GT(TRUE, x0[1]) → 932_0_POWER_GT(x0[1] / 2)

(0) -> (1), if (x0[0] > 1 ∧x0[0] →^* x0[1])

(1) -> (0), if (x0[1] / 2 →^* x0[0])

The set Q consists of the following terms:
932_0_power_GT(0)
1302_0_power_NE(0)
1302_0_power_NE(1)
1055_1_power_InvokeMethod(949_0_power_Return, x0, x1)

(15) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpDefaultShapeHeuristic@3b4b8082 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 932_0_POWER_GT(x0) → COND_932_0_POWER_GT(>(x0, 1), x0) the following chains were created:

We consider the chain 932_0_POWER_GT(x0[0]) → COND_932_0_POWER_GT(>(x0[0], 1), x0[0]), COND_932_0_POWER_GT(TRUE, x0[1]) → 932_0_POWER_GT(/(x0[1], 2)) which results in the following constraint:
(1)    (>(x0[0], 1)=TRUE∧x0[0]=x0[1] ⇒ 932_0_POWER_GT(x0[0])≥NonInfC∧932_0_POWER_GT(x0[0])≥COND_932_0_POWER_GT(>(x0[0], 1), x0[0])∧(U^Increasing(COND_932_0_POWER_GT(>(x0[0], 1), x0[0])), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2)    (>(x0[0], 1)=TRUE ⇒ 932_0_POWER_GT(x0[0])≥NonInfC∧932_0_POWER_GT(x0[0])≥COND_932_0_POWER_GT(>(x0[0], 1), x0[0])∧(U^Increasing(COND_932_0_POWER_GT(>(x0[0], 1), x0[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_932_0_POWER_GT(>(x0[0], 1), x0[0])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[0] ≥ 0∧[(-1)bso_19] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_932_0_POWER_GT(>(x0[0], 1), x0[0])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[0] ≥ 0∧[(-1)bso_19] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_932_0_POWER_GT(>(x0[0], 1), x0[0])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[0] ≥ 0∧[(-1)bso_19] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_932_0_POWER_GT(>(x0[0], 1), x0[0])), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x0[0] ≥ 0∧[(-1)bso_19] ≥ 0)

For Pair COND_932_0_POWER_GT(TRUE, x0) → 932_0_POWER_GT(/(x0, 2)) the following chains were created:

We consider the chain 932_0_POWER_GT(x0[0]) → COND_932_0_POWER_GT(>(x0[0], 1), x0[0]), COND_932_0_POWER_GT(TRUE, x0[1]) → 932_0_POWER_GT(/(x0[1], 2)), 932_0_POWER_GT(x0[0]) → COND_932_0_POWER_GT(>(x0[0], 1), x0[0]) which results in the following constraint:
(7)    (>(x0[0], 1)=TRUE∧x0[0]=x0[1]∧/(x0[1], 2)=x0[0]1 ⇒ COND_932_0_POWER_GT(TRUE, x0[1])≥NonInfC∧COND_932_0_POWER_GT(TRUE, x0[1])≥932_0_POWER_GT(/(x0[1], 2))∧(U^Increasing(932_0_POWER_GT(/(x0[1], 2))), ≥))

We simplified constraint (7) using rules (III), (IV) which results in the following new constraint:
(8)    (>(x0[0], 1)=TRUE ⇒ COND_932_0_POWER_GT(TRUE, x0[0])≥NonInfC∧COND_932_0_POWER_GT(TRUE, x0[0])≥932_0_POWER_GT(/(x0[0], 2))∧(U^Increasing(932_0_POWER_GT(/(x0[1], 2))), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(932_0_POWER_GT(/(x0[1], 2))), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[1 + (-1)bso_24] + x0[0] + [-1]max{x0[0], [-1]x0[0]} ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(932_0_POWER_GT(/(x0[1], 2))), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[1 + (-1)bso_24] + x0[0] + [-1]max{x0[0], [-1]x0[0]} ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    (x0[0] + [-2] ≥ 0∧[2]x0[0] ≥ 0 ⇒ (U^Increasing(932_0_POWER_GT(/(x0[1], 2))), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[1 + (-1)bso_24] ≥ 0)

We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(12)    (x0[0] ≥ 0∧[4] + [2]x0[0] ≥ 0 ⇒ (U^Increasing(932_0_POWER_GT(/(x0[1], 2))), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[1 + (-1)bso_24] ≥ 0)

We simplified constraint (12) using rule (IDP_POLY_GCD) which results in the following new constraint:
(13)    (x0[0] ≥ 0∧[2] + x0[0] ≥ 0 ⇒ (U^Increasing(932_0_POWER_GT(/(x0[1], 2))), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[1 + (-1)bso_24] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

932_0_POWER_GT(x0) → COND_932_0_POWER_GT(>(x0, 1), x0)
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_932_0_POWER_GT(>(x0[0], 1), x0[0])), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x0[0] ≥ 0∧[(-1)bso_19] ≥ 0)
COND_932_0_POWER_GT(TRUE, x0) → 932_0_POWER_GT(/(x0, 2))
- (x0[0] ≥ 0∧[2] + x0[0] ≥ 0 ⇒ (U^Increasing(932_0_POWER_GT(/(x0[1], 2))), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[1 + (-1)bso_24] ≥ 0)

POL(TRUE) = [1]
POL(FALSE) = 0
POL(932_0_power_GT(x₁)) = [-1] + [-1]x₁
POL(0) = 0
POL(949_0_power_Return) = [-1]
POL(1055_1_power_InvokeMethod(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂ + [-1]x₁
POL(1) = [1]
POL(1302_0_power_NE(x₁)) = [-1] + [-1]x₁
POL(2) = [2]
POL(932_0_POWER_GT(x₁)) = [-1] + x₁
POL(COND_932_0_POWER_GT(x₁, x₂)) = [-1] + x₂
POL(>(x₁, x₂)) = [-1]

Polynomial Interpretations with Context Sensitive Arithemetic Replacement
POL(Term^CSAR-Mode @ Context)

POL(/(x₁, 2)¹ @ {932_0_POWER_GT_1/0}) = max{x₁, [-1]x₁} + [-1]

The following pairs are in P_>:

COND_932_0_POWER_GT(TRUE, x0[1]) → 932_0_POWER_GT(/(x0[1], 2))

The following pairs are in P_bound:

932_0_POWER_GT(x0[0]) → COND_932_0_POWER_GT(>(x0[0], 1), x0[0])
COND_932_0_POWER_GT(TRUE, x0[1]) → 932_0_POWER_GT(/(x0[1], 2))

The following pairs are in P_≥:

932_0_POWER_GT(x0[0]) → COND_932_0_POWER_GT(>(x0[0], 1), x0[0])

At least the following rules have been oriented under context sensitive arithmetic replacement:

/¹ →

(16) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
932_0_power_GT(0) → 949_0_power_Return
1055_1_power_InvokeMethod(949_0_power_Return, x1, 1) → 1302_0_power_NE(x1 % 2)
1302_0_power_NE(0) → 949_0_power_Return
1302_0_power_NE(1) → 949_0_power_Return
1055_1_power_InvokeMethod(949_0_power_Return, x0, x1) → 1302_0_power_NE(x0 % 2)

The integer pair graph contains the following rules and edges:
(0): 932_0_POWER_GT(x0[0]) → COND_932_0_POWER_GT(x0[0] > 1, x0[0])

The set Q consists of the following terms:
932_0_power_GT(0)
1302_0_power_NE(0)
1302_0_power_NE(1)
1055_1_power_InvokeMethod(949_0_power_Return, x0, x1)

(17) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(18) TRUE

(19) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Power.main([Ljava/lang/String;)V
SCC calls the following helper methods: Power.power(II)I, Power.even(I)Z, Power.odd(I)Z
Performed SCC analyses: UsedFieldsAnalysis

(20) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 76 rules for P and 102 rules for R.

P rules:
2345_0_main_Load(EOS(STATIC_2345), java.lang.Object(ARRAY(i777)), i778, i778) → 2347_0_main_ArrayLength(EOS(STATIC_2347), java.lang.Object(ARRAY(i777)), i778, i778, java.lang.Object(ARRAY(i777)))
2347_0_main_ArrayLength(EOS(STATIC_2347), java.lang.Object(ARRAY(i777)), i778, i778, java.lang.Object(ARRAY(i777))) → 2348_0_main_GE(EOS(STATIC_2348), java.lang.Object(ARRAY(i777)), i778, i778, i777) | >=(i777, 0)
2348_0_main_GE(EOS(STATIC_2348), java.lang.Object(ARRAY(i777)), i778, i778, i777) → 2350_0_main_GE(EOS(STATIC_2350), java.lang.Object(ARRAY(i777)), i778, i778, i777)
2350_0_main_GE(EOS(STATIC_2350), java.lang.Object(ARRAY(i777)), i778, i778, i777) → 2353_0_main_Load(EOS(STATIC_2353), java.lang.Object(ARRAY(i777)), i778) | <(i778, i777)
2353_0_main_Load(EOS(STATIC_2353), java.lang.Object(ARRAY(i777)), i778) → 2356_0_main_ArrayLength(EOS(STATIC_2356), java.lang.Object(ARRAY(i777)), i778, java.lang.Object(ARRAY(i777)))
2356_0_main_ArrayLength(EOS(STATIC_2356), java.lang.Object(ARRAY(i777)), i778, java.lang.Object(ARRAY(i777))) → 2357_0_main_Load(EOS(STATIC_2357), java.lang.Object(ARRAY(i777)), i778, i777) | >=(i777, 0)
2357_0_main_Load(EOS(STATIC_2357), java.lang.Object(ARRAY(i777)), i778, i777) → 2358_0_main_Load(EOS(STATIC_2358), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(ARRAY(i777)))
2358_0_main_Load(EOS(STATIC_2358), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(ARRAY(i777))) → 2359_0_main_ArrayAccess(EOS(STATIC_2359), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(ARRAY(i777)), i778)
2359_0_main_ArrayAccess(EOS(STATIC_2359), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(ARRAY(i777)), i778) → 2361_0_main_ArrayAccess(EOS(STATIC_2361), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(ARRAY(i777)), i778)
2361_0_main_ArrayAccess(EOS(STATIC_2361), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(ARRAY(i777)), i778) → 2364_0_main_InvokeMethod(EOS(STATIC_2364), java.lang.Object(ARRAY(i777)), i778, i777, o728) | <(i778, i777)
2364_0_main_InvokeMethod(EOS(STATIC_2364), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(o731sub)) → 2366_0_main_InvokeMethod(EOS(STATIC_2366), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(o731sub))
2366_0_main_InvokeMethod(EOS(STATIC_2366), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(o731sub)) → 2369_0_length_Load(EOS(STATIC_2369), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(o731sub), java.lang.Object(o731sub))
2369_0_length_Load(EOS(STATIC_2369), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(o731sub), java.lang.Object(o731sub)) → 2377_0_length_FieldAccess(EOS(STATIC_2377), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(o731sub), java.lang.Object(o731sub))
2377_0_length_FieldAccess(EOS(STATIC_2377), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(java.lang.String(o736sub, i790)), java.lang.Object(java.lang.String(o736sub, i790))) → 2379_0_length_FieldAccess(EOS(STATIC_2379), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(java.lang.String(o736sub, i790)), java.lang.Object(java.lang.String(o736sub, i790))) | &&(>=(i790, 0), >=(i791, 0))
2379_0_length_FieldAccess(EOS(STATIC_2379), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(java.lang.String(o736sub, i790)), java.lang.Object(java.lang.String(o736sub, i790))) → 2383_0_length_Return(EOS(STATIC_2383), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(java.lang.String(o736sub, i790)), i790)
2383_0_length_Return(EOS(STATIC_2383), java.lang.Object(ARRAY(i777)), i778, i777, java.lang.Object(java.lang.String(o736sub, i790)), i790) → 2387_0_main_InvokeMethod(EOS(STATIC_2387), java.lang.Object(ARRAY(i777)), i778, i777, i790)
2387_0_main_InvokeMethod(EOS(STATIC_2387), java.lang.Object(ARRAY(i777)), i778, i777, i790) → 2389_1_main_InvokeMethod(2389_0_power_Load(EOS(STATIC_2389), i777, i790), java.lang.Object(ARRAY(i777)), i778, i777, i790)
2389_1_main_InvokeMethod(949_0_power_Return(EOS(STATIC_949), i795, matching1, matching2), java.lang.Object(ARRAY(i777)), i778, i795, matching3) → 2407_0_power_Return(EOS(STATIC_2407), java.lang.Object(ARRAY(i795)), i778, i795, 0, i795, 0, 1) | &&(&&(=(matching1, 0), =(matching2, 1)), =(matching3, 0))
2389_1_main_InvokeMethod(991_0_power_Return(EOS(STATIC_991), i796, matching1, i796), java.lang.Object(ARRAY(i777)), i778, i796, matching2) → 2408_0_power_Return(EOS(STATIC_2408), java.lang.Object(ARRAY(i796)), i778, i796, 1, i796, 1, i796) | &&(=(matching1, 1), =(matching2, 1))
2389_1_main_InvokeMethod(1328_0_power_Return(EOS(STATIC_1328), i797, i310, i310), java.lang.Object(ARRAY(i777)), i778, i797, i798) → 2409_0_power_Return(EOS(STATIC_2409), java.lang.Object(ARRAY(i797)), i778, i797, i798, i797, i310, i310)
2389_1_main_InvokeMethod(1338_0_power_Return(EOS(STATIC_1338), i363), java.lang.Object(ARRAY(i777)), i778, i799, i800) → 2410_0_power_Return(EOS(STATIC_2410), java.lang.Object(ARRAY(i799)), i778, i799, i800, i363)
2407_0_power_Return(EOS(STATIC_2407), java.lang.Object(ARRAY(i795)), i778, i795, matching1, i795, matching2, matching3) → 2414_0_main_InvokeMethod(EOS(STATIC_2414), java.lang.Object(ARRAY(i795)), i778, 1) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1))
2414_0_main_InvokeMethod(EOS(STATIC_2414), java.lang.Object(ARRAY(i795)), i778, matching1) → 2419_0_main_InvokeMethod(EOS(STATIC_2419), java.lang.Object(ARRAY(i795)), i778, 1) | =(matching1, 1)
2419_0_main_InvokeMethod(EOS(STATIC_2419), java.lang.Object(ARRAY(i797)), i778, i310) → 2421_0_main_InvokeMethod(EOS(STATIC_2421), java.lang.Object(ARRAY(i797)), i778, i310)
2421_0_main_InvokeMethod(EOS(STATIC_2421), java.lang.Object(ARRAY(i799)), i778, i363) → 2423_1_main_InvokeMethod(2423_0_even_Load(EOS(STATIC_2423), i363), java.lang.Object(ARRAY(i799)), i778, i363)
2423_1_main_InvokeMethod(1104_0_even_Return(EOS(STATIC_1104), matching1, matching2), java.lang.Object(ARRAY(i799)), i778, matching3) → 2442_0_even_Return(EOS(STATIC_2442), java.lang.Object(ARRAY(i799)), i778, 0, 0, 1) | &&(&&(=(matching1, 0), =(matching2, 1)), =(matching3, 0))
2423_1_main_InvokeMethod(1151_0_even_Return(EOS(STATIC_1151), matching1, matching2), java.lang.Object(ARRAY(i799)), i778, matching3) → 2444_0_even_Return(EOS(STATIC_2444), java.lang.Object(ARRAY(i799)), i778, 1, 1, 0) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 1))
2423_1_main_InvokeMethod(1276_0_even_Return(EOS(STATIC_1276), i337), java.lang.Object(ARRAY(i799)), i778, i812) → 2445_0_even_Return(EOS(STATIC_2445), java.lang.Object(ARRAY(i799)), i778, i812, i337)
2442_0_even_Return(EOS(STATIC_2442), java.lang.Object(ARRAY(i799)), i778, matching1, matching2, matching3) → 2454_0_main_StackPop(EOS(STATIC_2454), java.lang.Object(ARRAY(i799)), i778, 1) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1))
2454_0_main_StackPop(EOS(STATIC_2454), java.lang.Object(ARRAY(i799)), i778, matching1) → 2459_0_main_StackPop(EOS(STATIC_2459), java.lang.Object(ARRAY(i799)), i778, 1) | =(matching1, 1)
2459_0_main_StackPop(EOS(STATIC_2459), java.lang.Object(ARRAY(i799)), i778, i337) → 2464_0_main_Load(EOS(STATIC_2464), java.lang.Object(ARRAY(i799)), i778)
2464_0_main_Load(EOS(STATIC_2464), java.lang.Object(ARRAY(i799)), i778) → 2469_0_main_ArrayLength(EOS(STATIC_2469), java.lang.Object(ARRAY(i799)), i778, java.lang.Object(ARRAY(i799)))
2469_0_main_ArrayLength(EOS(STATIC_2469), java.lang.Object(ARRAY(i799)), i778, java.lang.Object(ARRAY(i799))) → 2474_0_main_Load(EOS(STATIC_2474), java.lang.Object(ARRAY(i799)), i778, i799) | >=(i799, 0)
2474_0_main_Load(EOS(STATIC_2474), java.lang.Object(ARRAY(i799)), i778, i799) → 2479_0_main_Load(EOS(STATIC_2479), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(ARRAY(i799)))
2479_0_main_Load(EOS(STATIC_2479), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(ARRAY(i799))) → 2483_0_main_ArrayAccess(EOS(STATIC_2483), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(ARRAY(i799)), i778)
2483_0_main_ArrayAccess(EOS(STATIC_2483), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(ARRAY(i799)), i778) → 2487_0_main_ArrayAccess(EOS(STATIC_2487), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(ARRAY(i799)), i778)
2487_0_main_ArrayAccess(EOS(STATIC_2487), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(ARRAY(i799)), i778) → 2493_0_main_InvokeMethod(EOS(STATIC_2493), java.lang.Object(ARRAY(i799)), i778, i799, o773) | <(i778, i799)
2493_0_main_InvokeMethod(EOS(STATIC_2493), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(o778sub)) → 2500_0_main_InvokeMethod(EOS(STATIC_2500), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(o778sub))
2500_0_main_InvokeMethod(EOS(STATIC_2500), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(o778sub)) → 2504_0_length_Load(EOS(STATIC_2504), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(o778sub), java.lang.Object(o778sub))
2504_0_length_Load(EOS(STATIC_2504), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(o778sub), java.lang.Object(o778sub)) → 2513_0_length_FieldAccess(EOS(STATIC_2513), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(o778sub), java.lang.Object(o778sub))
2513_0_length_FieldAccess(EOS(STATIC_2513), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(java.lang.String(o789sub, i829)), java.lang.Object(java.lang.String(o789sub, i829))) → 2515_0_length_FieldAccess(EOS(STATIC_2515), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(java.lang.String(o789sub, i829)), java.lang.Object(java.lang.String(o789sub, i829))) | &&(>=(i829, 0), >=(i830, 0))
2515_0_length_FieldAccess(EOS(STATIC_2515), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(java.lang.String(o789sub, i829)), java.lang.Object(java.lang.String(o789sub, i829))) → 2520_0_length_Return(EOS(STATIC_2520), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(java.lang.String(o789sub, i829)), i829)
2520_0_length_Return(EOS(STATIC_2520), java.lang.Object(ARRAY(i799)), i778, i799, java.lang.Object(java.lang.String(o789sub, i829)), i829) → 2524_0_main_InvokeMethod(EOS(STATIC_2524), java.lang.Object(ARRAY(i799)), i778, i799, i829)
2524_0_main_InvokeMethod(EOS(STATIC_2524), java.lang.Object(ARRAY(i799)), i778, i799, i829) → 2526_1_main_InvokeMethod(2526_0_power_Load(EOS(STATIC_2526), i799, i829), java.lang.Object(ARRAY(i799)), i778, i799, i829)
2526_1_main_InvokeMethod(949_0_power_Return(EOS(STATIC_949), i843, matching1, matching2), java.lang.Object(ARRAY(i799)), i778, i843, matching3) → 2545_0_power_Return(EOS(STATIC_2545), java.lang.Object(ARRAY(i843)), i778, i843, 0, i843, 0, 1) | &&(&&(=(matching1, 0), =(matching2, 1)), =(matching3, 0))
2526_1_main_InvokeMethod(991_0_power_Return(EOS(STATIC_991), i844, matching1, i844), java.lang.Object(ARRAY(i799)), i778, i844, matching2) → 2546_0_power_Return(EOS(STATIC_2546), java.lang.Object(ARRAY(i844)), i778, i844, 1, i844, 1, i844) | &&(=(matching1, 1), =(matching2, 1))
2526_1_main_InvokeMethod(1328_0_power_Return(EOS(STATIC_1328), i845, i310, i310), java.lang.Object(ARRAY(i799)), i778, i845, i846) → 2547_0_power_Return(EOS(STATIC_2547), java.lang.Object(ARRAY(i845)), i778, i845, i846, i845, i310, i310)
2526_1_main_InvokeMethod(1338_0_power_Return(EOS(STATIC_1338), i363), java.lang.Object(ARRAY(i799)), i778, i847, i848) → 2548_0_power_Return(EOS(STATIC_2548), java.lang.Object(ARRAY(i847)), i778, i847, i848, i363)
2545_0_power_Return(EOS(STATIC_2545), java.lang.Object(ARRAY(i843)), i778, i843, matching1, i843, matching2, matching3) → 2552_0_main_InvokeMethod(EOS(STATIC_2552), java.lang.Object(ARRAY(i843)), i778, 1) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1))
2552_0_main_InvokeMethod(EOS(STATIC_2552), java.lang.Object(ARRAY(i843)), i778, matching1) → 2557_0_main_InvokeMethod(EOS(STATIC_2557), java.lang.Object(ARRAY(i843)), i778, 1) | =(matching1, 1)
2557_0_main_InvokeMethod(EOS(STATIC_2557), java.lang.Object(ARRAY(i845)), i778, i310) → 2560_0_main_InvokeMethod(EOS(STATIC_2560), java.lang.Object(ARRAY(i845)), i778, i310)
2560_0_main_InvokeMethod(EOS(STATIC_2560), java.lang.Object(ARRAY(i847)), i778, i363) → 2562_1_main_InvokeMethod(2562_0_odd_Load(EOS(STATIC_2562), i363), java.lang.Object(ARRAY(i847)), i778, i363)
2562_1_main_InvokeMethod(1561_0_odd_Return(EOS(STATIC_1561), matching1, matching2), java.lang.Object(ARRAY(i847)), i778, matching3) → 2588_0_odd_Return(EOS(STATIC_2588), java.lang.Object(ARRAY(i847)), i778, 0, 0, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
2562_1_main_InvokeMethod(1604_0_odd_Return(EOS(STATIC_1604), matching1, matching2), java.lang.Object(ARRAY(i847)), i778, matching3) → 2589_0_odd_Return(EOS(STATIC_2589), java.lang.Object(ARRAY(i847)), i778, 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
2562_1_main_InvokeMethod(1665_0_odd_Return(EOS(STATIC_1665), i337), java.lang.Object(ARRAY(i847)), i778, i874) → 2591_0_odd_Return(EOS(STATIC_2591), java.lang.Object(ARRAY(i847)), i778, i874, i337)
2588_0_odd_Return(EOS(STATIC_2588), java.lang.Object(ARRAY(i847)), i778, matching1, matching2, matching3) → 2599_0_main_StackPop(EOS(STATIC_2599), java.lang.Object(ARRAY(i847)), i778, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
2599_0_main_StackPop(EOS(STATIC_2599), java.lang.Object(ARRAY(i847)), i778, matching1) → 2604_0_main_StackPop(EOS(STATIC_2604), java.lang.Object(ARRAY(i847)), i778, 0) | =(matching1, 0)
2604_0_main_StackPop(EOS(STATIC_2604), java.lang.Object(ARRAY(i847)), i778, i337) → 2611_0_main_Inc(EOS(STATIC_2611), java.lang.Object(ARRAY(i847)), i778)
2611_0_main_Inc(EOS(STATIC_2611), java.lang.Object(ARRAY(i847)), i778) → 2618_0_main_JMP(EOS(STATIC_2618), java.lang.Object(ARRAY(i847)), +(i778, 1)) | >=(i778, 0)
2618_0_main_JMP(EOS(STATIC_2618), java.lang.Object(ARRAY(i847)), i894) → 2624_0_main_Load(EOS(STATIC_2624), java.lang.Object(ARRAY(i847)), i894)
2624_0_main_Load(EOS(STATIC_2624), java.lang.Object(ARRAY(i847)), i894) → 2341_0_main_Load(EOS(STATIC_2341), java.lang.Object(ARRAY(i847)), i894)
2341_0_main_Load(EOS(STATIC_2341), java.lang.Object(ARRAY(i777)), i778) → 2345_0_main_Load(EOS(STATIC_2345), java.lang.Object(ARRAY(i777)), i778, i778)
2589_0_odd_Return(EOS(STATIC_2589), java.lang.Object(ARRAY(i847)), i778, matching1, matching2, matching3) → 2601_0_main_StackPop(EOS(STATIC_2601), java.lang.Object(ARRAY(i847)), i778, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
2601_0_main_StackPop(EOS(STATIC_2601), java.lang.Object(ARRAY(i847)), i778, matching1) → 2604_0_main_StackPop(EOS(STATIC_2604), java.lang.Object(ARRAY(i847)), i778, 1) | =(matching1, 1)
2591_0_odd_Return(EOS(STATIC_2591), java.lang.Object(ARRAY(i847)), i778, i874, i337) → 2604_0_main_StackPop(EOS(STATIC_2604), java.lang.Object(ARRAY(i847)), i778, i337)
2546_0_power_Return(EOS(STATIC_2546), java.lang.Object(ARRAY(i844)), i778, i844, matching1, i844, matching2, i844) → 2554_0_main_InvokeMethod(EOS(STATIC_2554), java.lang.Object(ARRAY(i844)), i778, i844) | &&(=(matching1, 1), =(matching2, 1))
2554_0_main_InvokeMethod(EOS(STATIC_2554), java.lang.Object(ARRAY(i844)), i778, i844) → 2557_0_main_InvokeMethod(EOS(STATIC_2557), java.lang.Object(ARRAY(i844)), i778, i844)
2547_0_power_Return(EOS(STATIC_2547), java.lang.Object(ARRAY(i845)), i778, i845, i846, i845, i310, i310) → 2557_0_main_InvokeMethod(EOS(STATIC_2557), java.lang.Object(ARRAY(i845)), i778, i310)
2548_0_power_Return(EOS(STATIC_2548), java.lang.Object(ARRAY(i847)), i778, i847, i848, i363) → 2560_0_main_InvokeMethod(EOS(STATIC_2560), java.lang.Object(ARRAY(i847)), i778, i363)
2444_0_even_Return(EOS(STATIC_2444), java.lang.Object(ARRAY(i799)), i778, matching1, matching2, matching3) → 2456_0_main_StackPop(EOS(STATIC_2456), java.lang.Object(ARRAY(i799)), i778, 0) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 0))
2456_0_main_StackPop(EOS(STATIC_2456), java.lang.Object(ARRAY(i799)), i778, matching1) → 2459_0_main_StackPop(EOS(STATIC_2459), java.lang.Object(ARRAY(i799)), i778, 0) | =(matching1, 0)
2445_0_even_Return(EOS(STATIC_2445), java.lang.Object(ARRAY(i799)), i778, i812, i337) → 2459_0_main_StackPop(EOS(STATIC_2459), java.lang.Object(ARRAY(i799)), i778, i337)
2408_0_power_Return(EOS(STATIC_2408), java.lang.Object(ARRAY(i796)), i778, i796, matching1, i796, matching2, i796) → 2416_0_main_InvokeMethod(EOS(STATIC_2416), java.lang.Object(ARRAY(i796)), i778, i796) | &&(=(matching1, 1), =(matching2, 1))
2416_0_main_InvokeMethod(EOS(STATIC_2416), java.lang.Object(ARRAY(i796)), i778, i796) → 2419_0_main_InvokeMethod(EOS(STATIC_2419), java.lang.Object(ARRAY(i796)), i778, i796)
2409_0_power_Return(EOS(STATIC_2409), java.lang.Object(ARRAY(i797)), i778, i797, i798, i797, i310, i310) → 2419_0_main_InvokeMethod(EOS(STATIC_2419), java.lang.Object(ARRAY(i797)), i778, i310)
2410_0_power_Return(EOS(STATIC_2410), java.lang.Object(ARRAY(i799)), i778, i799, i800, i363) → 2421_0_main_InvokeMethod(EOS(STATIC_2421), java.lang.Object(ARRAY(i799)), i778, i363)
R rules:
2389_0_power_Load(EOS(STATIC_2389), i777, i790) → 2393_0_power_Load(EOS(STATIC_2393), i777, i790)
2393_0_power_Load(EOS(STATIC_2393), i777, i790) → 926_0_power_Load(EOS(STATIC_926), i777, i790)
2423_0_even_Load(EOS(STATIC_2423), i363) → 2428_0_even_Load(EOS(STATIC_2428), i363)
2428_0_even_Load(EOS(STATIC_2428), i363) → 1075_0_even_Load(EOS(STATIC_1075), i363)
2526_0_power_Load(EOS(STATIC_2526), i799, i829) → 2532_0_power_Load(EOS(STATIC_2532), i799, i829)
2532_0_power_Load(EOS(STATIC_2532), i799, i829) → 926_0_power_Load(EOS(STATIC_926), i799, i829)
2562_0_odd_Load(EOS(STATIC_2562), i363) → 2568_0_odd_Load(EOS(STATIC_2568), i363)
2568_0_odd_Load(EOS(STATIC_2568), i363) → 1516_0_odd_Load(EOS(STATIC_1516), i363)
1064_0_power_Load(EOS(STATIC_1064), i269) → 926_0_power_Load(EOS(STATIC_926), i269, i276)
1216_0_odd_Load(EOS(STATIC_1216), i306) → 1516_0_odd_Load(EOS(STATIC_1516), i306)
1643_0_even_Load(EOS(STATIC_1643)) → 1075_0_even_Load(EOS(STATIC_1075), i497)
926_0_power_Load(EOS(STATIC_926), i246, i247) → 932_0_power_GT(EOS(STATIC_932), i246, i247, i247)
932_0_power_GT(EOS(STATIC_932), i246, matching1, matching2) → 937_0_power_GT(EOS(STATIC_937), i246, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
932_0_power_GT(EOS(STATIC_932), i246, i259, i259) → 939_0_power_GT(EOS(STATIC_939), i246, i259, i259)
937_0_power_GT(EOS(STATIC_937), i246, matching1, matching2) → 941_0_power_ConstantStackPush(EOS(STATIC_941), i246, 0) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
939_0_power_GT(EOS(STATIC_939), i246, i259, i259) → 942_0_power_Load(EOS(STATIC_942), i246, i259) | >(i259, 0)
941_0_power_ConstantStackPush(EOS(STATIC_941), i246, matching1) → 949_0_power_Return(EOS(STATIC_949), i246, 0, 1) | =(matching1, 0)
942_0_power_Load(EOS(STATIC_942), i246, i259) → 950_0_power_ConstantStackPush(EOS(STATIC_950), i246, i259, i259)
950_0_power_ConstantStackPush(EOS(STATIC_950), i246, i259, i259) → 959_0_power_NE(EOS(STATIC_959), i246, i259, i259, 1)
959_0_power_NE(EOS(STATIC_959), i246, matching1, matching2, matching3) → 969_0_power_NE(EOS(STATIC_969), i246, 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
959_0_power_NE(EOS(STATIC_959), i246, i263, i263, matching1) → 970_0_power_NE(EOS(STATIC_970), i246, i263, i263, 1) | =(matching1, 1)
969_0_power_NE(EOS(STATIC_969), i246, matching1, matching2, matching3) → 978_0_power_Load(EOS(STATIC_978), i246, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
970_0_power_NE(EOS(STATIC_970), i246, i263, i263, matching1) → 979_0_power_Load(EOS(STATIC_979), i246, i263) | &&(!(=(i263, 1)), =(matching1, 1))
978_0_power_Load(EOS(STATIC_978), i246, matching1) → 991_0_power_Return(EOS(STATIC_991), i246, 1, i246) | =(matching1, 1)
979_0_power_Load(EOS(STATIC_979), i246, i263) → 992_0_power_Load(EOS(STATIC_992), i246, i263, i246)
992_0_power_Load(EOS(STATIC_992), i246, i263, i246) → 1002_0_power_IntArithmetic(EOS(STATIC_1002), i246, i263, i246, i246)
1002_0_power_IntArithmetic(EOS(STATIC_1002), i246, i263, i246, i246) → 1013_0_power_Load(EOS(STATIC_1013), i246, i263, *(i246, i246))
1013_0_power_Load(EOS(STATIC_1013), i246, i263, i269) → 1021_0_power_ConstantStackPush(EOS(STATIC_1021), i246, i263, i269, i263)
1021_0_power_ConstantStackPush(EOS(STATIC_1021), i246, i263, i269, i263) → 1035_0_power_IntArithmetic(EOS(STATIC_1035), i246, i263, i269, i263)
1035_0_power_IntArithmetic(EOS(STATIC_1035), i246, i263, i269, i263) → 1046_0_power_InvokeMethod(EOS(STATIC_1046), i246, i263, i269) | >(i263, 1)
1046_0_power_InvokeMethod(EOS(STATIC_1046), i246, i263, i269) → 1055_1_power_InvokeMethod(1055_0_power_Load(EOS(STATIC_1055), i269), i246, i263, i269)
1055_0_power_Load(EOS(STATIC_1055), i269) → 1064_0_power_Load(EOS(STATIC_1064), i269)
1055_1_power_InvokeMethod(991_0_power_Return(EOS(STATIC_991), i285, matching1, i285), i246, i263, i285) → 1093_0_power_Return(EOS(STATIC_1093), i246, i263, i285, i285, i285) | =(matching1, 1)
1055_1_power_InvokeMethod(1328_0_power_Return(EOS(STATIC_1328), i368, i310, i310), i246, i263, i368) → 1355_0_power_Return(EOS(STATIC_1355), i246, i263, i368, i368, i310, i310)
1055_1_power_InvokeMethod(1338_0_power_Return(EOS(STATIC_1338), i363), i246, i263, i380) → 1373_0_power_Return(EOS(STATIC_1373), i246, i263, i380, i363)
1093_0_power_Return(EOS(STATIC_1093), i246, i263, i285, i285, i285) → 1100_0_power_Store(EOS(STATIC_1100), i246, i263, i285)
1100_0_power_Store(EOS(STATIC_1100), i246, i263, i285) → 1259_0_power_Store(EOS(STATIC_1259), i246, i263, i285)
1235_0_power_Return(EOS(STATIC_1235), i246, i263, i315, i315, i285, i285) → 1259_0_power_Store(EOS(STATIC_1259), i246, i263, i285)
1259_0_power_Store(EOS(STATIC_1259), i246, i263, i285) → 1282_0_power_Store(EOS(STATIC_1282), i246, i263, i285)
1269_0_power_Return(EOS(STATIC_1269), i246, i263, i329, i310) → 1282_0_power_Store(EOS(STATIC_1282), i246, i263, i310)
1282_0_power_Store(EOS(STATIC_1282), i246, i263, i310) → 1287_0_power_Load(EOS(STATIC_1287), i246, i263, i310)
1287_0_power_Load(EOS(STATIC_1287), i246, i263, i310) → 1292_0_power_ConstantStackPush(EOS(STATIC_1292), i246, i310, i263)
1292_0_power_ConstantStackPush(EOS(STATIC_1292), i246, i310, i263) → 1295_0_power_IntArithmetic(EOS(STATIC_1295), i246, i310, i263, 2)
1295_0_power_IntArithmetic(EOS(STATIC_1295), i246, i310, i263, matching1) → 1302_0_power_NE(EOS(STATIC_1302), i246, i310, %(i263, 2)) | =(matching1, 2)
1302_0_power_NE(EOS(STATIC_1302), i246, i310, matching1) → 1307_0_power_NE(EOS(STATIC_1307), i246, i310, 1) | =(matching1, 1)
1302_0_power_NE(EOS(STATIC_1302), i246, i310, matching1) → 1308_0_power_NE(EOS(STATIC_1308), i246, i310, 0) | =(matching1, 0)
1307_0_power_NE(EOS(STATIC_1307), i246, i310, matching1) → 1320_0_power_Load(EOS(STATIC_1320), i246, i310) | &&(>(1, 0), =(matching1, 1))
1308_0_power_NE(EOS(STATIC_1308), i246, i310, matching1) → 1321_0_power_Load(EOS(STATIC_1321), i246, i310) | =(matching1, 0)
1320_0_power_Load(EOS(STATIC_1320), i246, i310) → 1327_0_power_Load(EOS(STATIC_1327), i310, i246)
1321_0_power_Load(EOS(STATIC_1321), i246, i310) → 1328_0_power_Return(EOS(STATIC_1328), i246, i310, i310)
1327_0_power_Load(EOS(STATIC_1327), i310, i246) → 1332_0_power_IntArithmetic(EOS(STATIC_1332), i246, i310)
1332_0_power_IntArithmetic(EOS(STATIC_1332), i246, i310) → 1338_0_power_Return(EOS(STATIC_1338), *(i246, i310))
1355_0_power_Return(EOS(STATIC_1355), i246, i263, i368, i368, i310, i310) → 1235_0_power_Return(EOS(STATIC_1235), i246, i263, i368, i368, i310, i310)
1373_0_power_Return(EOS(STATIC_1373), i246, i263, i380, i363) → 1269_0_power_Return(EOS(STATIC_1269), i246, i263, i380, i363)
1075_0_even_Load(EOS(STATIC_1075), i278) → 1081_0_even_GT(EOS(STATIC_1081), i278, i278)
1081_0_even_GT(EOS(STATIC_1081), matching1, matching2) → 1089_0_even_GT(EOS(STATIC_1089), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
1081_0_even_GT(EOS(STATIC_1081), i286, i286) → 1090_0_even_GT(EOS(STATIC_1090), i286, i286)
1089_0_even_GT(EOS(STATIC_1089), matching1, matching2) → 1096_0_even_ConstantStackPush(EOS(STATIC_1096), 0) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
1090_0_even_GT(EOS(STATIC_1090), i286, i286) → 1098_0_even_Load(EOS(STATIC_1098), i286) | >(i286, 0)
1096_0_even_ConstantStackPush(EOS(STATIC_1096), matching1) → 1104_0_even_Return(EOS(STATIC_1104), 0, 1) | =(matching1, 0)
1098_0_even_Load(EOS(STATIC_1098), i286) → 1105_0_even_ConstantStackPush(EOS(STATIC_1105), i286, i286)
1105_0_even_ConstantStackPush(EOS(STATIC_1105), i286, i286) → 1114_0_even_NE(EOS(STATIC_1114), i286, i286, 1)
1114_0_even_NE(EOS(STATIC_1114), matching1, matching2, matching3) → 1125_0_even_NE(EOS(STATIC_1125), 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
1114_0_even_NE(EOS(STATIC_1114), i288, i288, matching1) → 1126_0_even_NE(EOS(STATIC_1126), i288, i288, 1) | =(matching1, 1)
1125_0_even_NE(EOS(STATIC_1125), matching1, matching2, matching3) → 1140_0_even_ConstantStackPush(EOS(STATIC_1140), 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
1126_0_even_NE(EOS(STATIC_1126), i288, i288, matching1) → 1142_0_even_Load(EOS(STATIC_1142), i288) | &&(!(=(i288, 1)), =(matching1, 1))
1140_0_even_ConstantStackPush(EOS(STATIC_1140), matching1) → 1151_0_even_Return(EOS(STATIC_1151), 1, 0) | =(matching1, 1)
1142_0_even_Load(EOS(STATIC_1142), i288) → 1152_0_even_ConstantStackPush(EOS(STATIC_1152), i288)
1152_0_even_ConstantStackPush(EOS(STATIC_1152), i288) → 1165_0_even_IntArithmetic(EOS(STATIC_1165), i288, 1)
1165_0_even_IntArithmetic(EOS(STATIC_1165), i288, matching1) → 1186_0_even_InvokeMethod(EOS(STATIC_1186), -(i288, 1)) | &&(>(i288, 0), =(matching1, 1))
1186_0_even_InvokeMethod(EOS(STATIC_1186), i306) → 1206_1_even_InvokeMethod(1206_0_odd_Load(EOS(STATIC_1206), i306), i306)
1206_0_odd_Load(EOS(STATIC_1206), i306) → 1216_0_odd_Load(EOS(STATIC_1216), i306)
1206_1_even_InvokeMethod(1604_0_odd_Return(EOS(STATIC_1604), matching1, matching2), matching3) → 1638_0_odd_Return(EOS(STATIC_1638), 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
1206_1_even_InvokeMethod(1665_0_odd_Return(EOS(STATIC_1665), i337), i513) → 1679_0_odd_Return(EOS(STATIC_1679), i513, i337)
1261_0_odd_Return(EOS(STATIC_1261), matching1, matching2, matching3) → 1273_0_even_Return(EOS(STATIC_1273), 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
1267_0_odd_Return(EOS(STATIC_1267), i338, i337) → 1276_0_even_Return(EOS(STATIC_1276), i337)
1273_0_even_Return(EOS(STATIC_1273), matching1) → 1276_0_even_Return(EOS(STATIC_1276), 1) | =(matching1, 1)
1638_0_odd_Return(EOS(STATIC_1638), matching1, matching2, matching3) → 1261_0_odd_Return(EOS(STATIC_1261), 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
1679_0_odd_Return(EOS(STATIC_1679), i513, i337) → 1267_0_odd_Return(EOS(STATIC_1267), i513, i337)
1516_0_odd_Load(EOS(STATIC_1516), i450) → 1525_0_odd_GT(EOS(STATIC_1525), i450, i450)
1525_0_odd_GT(EOS(STATIC_1525), matching1, matching2) → 1541_0_odd_GT(EOS(STATIC_1541), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
1525_0_odd_GT(EOS(STATIC_1525), i468, i468) → 1542_0_odd_GT(EOS(STATIC_1542), i468, i468)
1541_0_odd_GT(EOS(STATIC_1541), matching1, matching2) → 1551_0_odd_ConstantStackPush(EOS(STATIC_1551), 0) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
1542_0_odd_GT(EOS(STATIC_1542), i468, i468) → 1552_0_odd_Load(EOS(STATIC_1552), i468) | >(i468, 0)
1551_0_odd_ConstantStackPush(EOS(STATIC_1551), matching1) → 1561_0_odd_Return(EOS(STATIC_1561), 0, 0) | =(matching1, 0)
1552_0_odd_Load(EOS(STATIC_1552), i468) → 1563_0_odd_ConstantStackPush(EOS(STATIC_1563), i468, i468)
1563_0_odd_ConstantStackPush(EOS(STATIC_1563), i468, i468) → 1574_0_odd_NE(EOS(STATIC_1574), i468, i468, 1)
1574_0_odd_NE(EOS(STATIC_1574), matching1, matching2, matching3) → 1584_0_odd_NE(EOS(STATIC_1584), 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
1574_0_odd_NE(EOS(STATIC_1574), i488, i488, matching1) → 1585_0_odd_NE(EOS(STATIC_1585), i488, i488, 1) | =(matching1, 1)
1584_0_odd_NE(EOS(STATIC_1584), matching1, matching2, matching3) → 1596_0_odd_ConstantStackPush(EOS(STATIC_1596), 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
1585_0_odd_NE(EOS(STATIC_1585), i488, i488, matching1) → 1597_0_odd_Load(EOS(STATIC_1597), i488) | &&(!(=(i488, 1)), =(matching1, 1))
1596_0_odd_ConstantStackPush(EOS(STATIC_1596), matching1) → 1604_0_odd_Return(EOS(STATIC_1604), 1, 1) | =(matching1, 1)
1597_0_odd_Load(EOS(STATIC_1597), i488) → 1605_0_odd_ConstantStackPush(EOS(STATIC_1605), i488)
1605_0_odd_ConstantStackPush(EOS(STATIC_1605), i488) → 1613_0_odd_IntArithmetic(EOS(STATIC_1613), i488, 1)
1613_0_odd_IntArithmetic(EOS(STATIC_1613), i488, matching1) → 1624_0_odd_InvokeMethod(EOS(STATIC_1624)) | &&(>(i488, 0), =(matching1, 1))
1624_0_odd_InvokeMethod(EOS(STATIC_1624)) → 1640_1_odd_InvokeMethod(1640_0_even_Load(EOS(STATIC_1640)))
1640_0_even_Load(EOS(STATIC_1640)) → 1643_0_even_Load(EOS(STATIC_1643))
1640_1_odd_InvokeMethod(1151_0_even_Return(EOS(STATIC_1151), matching1, matching2)) → 1656_0_even_Return(EOS(STATIC_1656), 0) | &&(=(matching1, 1), =(matching2, 0))
1640_1_odd_InvokeMethod(1276_0_even_Return(EOS(STATIC_1276), i337)) → 1657_0_even_Return(EOS(STATIC_1657), i337)
1656_0_even_Return(EOS(STATIC_1656), matching1) → 1662_0_odd_Return(EOS(STATIC_1662), 0) | =(matching1, 0)
1657_0_even_Return(EOS(STATIC_1657), i337) → 1665_0_odd_Return(EOS(STATIC_1665), i337)
1662_0_odd_Return(EOS(STATIC_1662), matching1) → 1665_0_odd_Return(EOS(STATIC_1665), 0) | =(matching1, 0)

Combined rules. Obtained 14 conditional rules for P and 22 conditional rules for R.

P rules:
2389_1_main_InvokeMethod(1338_0_power_Return(EOS(STATIC_1338), x0), java.lang.Object(ARRAY(x1)), x2, x3, x4) → 2423_1_main_InvokeMethod(2423_0_even_Load(EOS(STATIC_2423), x0), java.lang.Object(ARRAY(x3)), x2, x0)
2389_1_main_InvokeMethod(1328_0_power_Return(EOS(STATIC_1328), x0, x1, x1), java.lang.Object(ARRAY(x2)), x3, x0, x4) → 2423_1_main_InvokeMethod(2423_0_even_Load(EOS(STATIC_2423), x1), java.lang.Object(ARRAY(x0)), x3, x1)
2389_1_main_InvokeMethod(949_0_power_Return(EOS(STATIC_949), x0, 0, 1), java.lang.Object(ARRAY(x3)), x4, x0, 0) → 2423_1_main_InvokeMethod(2423_0_even_Load(EOS(STATIC_2423), 1), java.lang.Object(ARRAY(x0)), x4, 1)
2423_1_main_InvokeMethod(1276_0_even_Return(EOS(STATIC_1276), x0), java.lang.Object(ARRAY(x1)), x2, x3) → 2526_1_main_InvokeMethod(2526_0_power_Load(EOS(STATIC_2526), x1, x4), java.lang.Object(ARRAY(x1)), x2, x1, x4) | &&(&&(>(+(x4, 1), 0), <(x2, x1)), >(+(x1, 1), 0))
2423_1_main_InvokeMethod(1104_0_even_Return(EOS(STATIC_1104), 0, 1), java.lang.Object(ARRAY(x2)), x3, 0) → 2526_1_main_InvokeMethod(2526_0_power_Load(EOS(STATIC_2526), x2, x5), java.lang.Object(ARRAY(x2)), x3, x2, x5) | &&(&&(>(+(x5, 1), 0), <(x3, x2)), >(+(x2, 1), 0))
2526_1_main_InvokeMethod(1338_0_power_Return(EOS(STATIC_1338), x0), java.lang.Object(ARRAY(x1)), x2, x3, x4) → 2562_1_main_InvokeMethod(2562_0_odd_Load(EOS(STATIC_2562), x0), java.lang.Object(ARRAY(x3)), x2, x0)
2526_1_main_InvokeMethod(1328_0_power_Return(EOS(STATIC_1328), x0, x1, x1), java.lang.Object(ARRAY(x2)), x3, x0, x4) → 2562_1_main_InvokeMethod(2562_0_odd_Load(EOS(STATIC_2562), x1), java.lang.Object(ARRAY(x0)), x3, x1)
2526_1_main_InvokeMethod(949_0_power_Return(EOS(STATIC_949), x0, 0, 1), java.lang.Object(ARRAY(x3)), x4, x0, 0) → 2562_1_main_InvokeMethod(2562_0_odd_Load(EOS(STATIC_2562), 1), java.lang.Object(ARRAY(x0)), x4, 1)
2562_1_main_InvokeMethod(1665_0_odd_Return(EOS(STATIC_1665), x0), java.lang.Object(ARRAY(x1)), x2, x3) → 2389_1_main_InvokeMethod(2389_0_power_Load(EOS(STATIC_2389), x1, x4), java.lang.Object(ARRAY(x1)), +(x2, 1), x1, x4) | &&(&&(&&(>(+(x4, 1), 0), >(+(x2, 1), 0)), >(+(x1, 1), 0)), >(x1, +(x2, 1)))
2562_1_main_InvokeMethod(1561_0_odd_Return(EOS(STATIC_1561), 0, 0), java.lang.Object(ARRAY(x2)), x3, 0) → 2389_1_main_InvokeMethod(2389_0_power_Load(EOS(STATIC_2389), x2, x5), java.lang.Object(ARRAY(x2)), +(x3, 1), x2, x5) | &&(&&(&&(>(+(x5, 1), 0), >(+(x3, 1), 0)), >(+(x2, 1), 0)), >(x2, +(x3, 1)))
2562_1_main_InvokeMethod(1604_0_odd_Return(EOS(STATIC_1604), 1, 1), java.lang.Object(ARRAY(x2)), x3, 1) → 2389_1_main_InvokeMethod(2389_0_power_Load(EOS(STATIC_2389), x2, x5), java.lang.Object(ARRAY(x2)), +(x3, 1), x2, x5) | &&(&&(&&(>(+(x5, 1), 0), >(+(x3, 1), 0)), >(+(x2, 1), 0)), >(x2, +(x3, 1)))
2526_1_main_InvokeMethod(991_0_power_Return(EOS(STATIC_991), x0, 1, x0), java.lang.Object(ARRAY(x2)), x3, x0, 1) → 2562_1_main_InvokeMethod(2562_0_odd_Load(EOS(STATIC_2562), x0), java.lang.Object(ARRAY(x0)), x3, x0)
2423_1_main_InvokeMethod(1151_0_even_Return(EOS(STATIC_1151), 1, 0), java.lang.Object(ARRAY(x2)), x3, 1) → 2526_1_main_InvokeMethod(2526_0_power_Load(EOS(STATIC_2526), x2, x5), java.lang.Object(ARRAY(x2)), x3, x2, x5) | &&(&&(>(+(x5, 1), 0), <(x3, x2)), >(+(x2, 1), 0))
2389_1_main_InvokeMethod(991_0_power_Return(EOS(STATIC_991), x0, 1, x0), java.lang.Object(ARRAY(x2)), x3, x0, 1) → 2423_1_main_InvokeMethod(2423_0_even_Load(EOS(STATIC_2423), x0), java.lang.Object(ARRAY(x0)), x3, x0)
R rules:
2389_0_power_Load(EOS(STATIC_2389), x0, x1) → 932_0_power_GT(EOS(STATIC_932), x0, x1, x1)
2423_0_even_Load(EOS(STATIC_2423), x0) → 1081_0_even_GT(EOS(STATIC_1081), x0, x0)
2526_0_power_Load(EOS(STATIC_2526), x0, x1) → 932_0_power_GT(EOS(STATIC_932), x0, x1, x1)
2562_0_odd_Load(EOS(STATIC_2562), x0) → 1525_0_odd_GT(EOS(STATIC_1525), x0, x0)
932_0_power_GT(EOS(STATIC_932), x0, 0, 0) → 949_0_power_Return(EOS(STATIC_949), x0, 0, 1)
932_0_power_GT(EOS(STATIC_932), x0, 1, 1) → 991_0_power_Return(EOS(STATIC_991), x0, 1, x0)
932_0_power_GT(EOS(STATIC_932), x0, x1, x1) → 1055_1_power_InvokeMethod(932_0_power_GT(EOS(STATIC_932), *(x0, x0), x2, x2), x0, x1, *(x0, x0)) | >(x1, 1)
1055_1_power_InvokeMethod(991_0_power_Return(EOS(STATIC_991), x0, 1, x0), x2, x3, x0) → 1302_0_power_NE(EOS(STATIC_1302), x2, x0, %(x3, 2))
1302_0_power_NE(EOS(STATIC_1302), x0, x1, 0) → 1328_0_power_Return(EOS(STATIC_1328), x0, x1, x1)
1302_0_power_NE(EOS(STATIC_1302), x0, x1, 1) → 1338_0_power_Return(EOS(STATIC_1338), *(x0, x1))
1055_1_power_InvokeMethod(1328_0_power_Return(EOS(STATIC_1328), x0, x1, x1), x2, x3, x0) → 1302_0_power_NE(EOS(STATIC_1302), x2, x1, %(x3, 2))
1055_1_power_InvokeMethod(1338_0_power_Return(EOS(STATIC_1338), x0), x1, x2, x3) → 1302_0_power_NE(EOS(STATIC_1302), x1, x0, %(x2, 2))
1081_0_even_GT(EOS(STATIC_1081), 0, 0) → 1104_0_even_Return(EOS(STATIC_1104), 0, 1)
1081_0_even_GT(EOS(STATIC_1081), 1, 1) → 1151_0_even_Return(EOS(STATIC_1151), 1, 0)
1081_0_even_GT(EOS(STATIC_1081), x0, x0) → 1206_1_even_InvokeMethod(1525_0_odd_GT(EOS(STATIC_1525), -(x0, 1), -(x0, 1)), -(x0, 1)) | &&(>(x0, 0), !(=(x0, 1)))
1206_1_even_InvokeMethod(1604_0_odd_Return(EOS(STATIC_1604), 1, 1), 1) → 1276_0_even_Return(EOS(STATIC_1276), 1)
1206_1_even_InvokeMethod(1665_0_odd_Return(EOS(STATIC_1665), x0), x1) → 1276_0_even_Return(EOS(STATIC_1276), x0)
1525_0_odd_GT(EOS(STATIC_1525), 0, 0) → 1561_0_odd_Return(EOS(STATIC_1561), 0, 0)
1525_0_odd_GT(EOS(STATIC_1525), 1, 1) → 1604_0_odd_Return(EOS(STATIC_1604), 1, 1)
1525_0_odd_GT(EOS(STATIC_1525), x0, x0) → 1640_1_odd_InvokeMethod(1081_0_even_GT(EOS(STATIC_1081), x1, x1)) | &&(>(x0, 0), !(=(x0, 1)))
1640_1_odd_InvokeMethod(1276_0_even_Return(EOS(STATIC_1276), x0)) → 1665_0_odd_Return(EOS(STATIC_1665), x0)
1640_1_odd_InvokeMethod(1151_0_even_Return(EOS(STATIC_1151), 1, 0)) → 1665_0_odd_Return(EOS(STATIC_1665), 0)

Filtered ground terms:

2423_0_even_Load(x1, x2) → 2423_0_even_Load(x2)
991_0_power_Return(x1, x2, x3, x4) → 991_0_power_Return(x2, x4)
2526_0_power_Load(x1, x2, x3) → 2526_0_power_Load(x2, x3)
Cond_2423_1_main_InvokeMethod2(x1, x2, x3, x4, x5, x6) → Cond_2423_1_main_InvokeMethod2(x1, x3, x4, x6)
1151_0_even_Return(x1, x2, x3) → 1151_0_even_Return
2562_0_odd_Load(x1, x2) → 2562_0_odd_Load(x2)
2389_0_power_Load(x1, x2, x3) → 2389_0_power_Load(x2, x3)
Cond_2562_1_main_InvokeMethod2(x1, x2, x3, x4, x5, x6) → Cond_2562_1_main_InvokeMethod2(x1, x3, x4, x6)
1604_0_odd_Return(x1, x2, x3) → 1604_0_odd_Return
Cond_2562_1_main_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_2562_1_main_InvokeMethod1(x1, x3, x4, x6)
1561_0_odd_Return(x1, x2, x3) → 1561_0_odd_Return
1665_0_odd_Return(x1, x2) → 1665_0_odd_Return(x2)
949_0_power_Return(x1, x2, x3, x4) → 949_0_power_Return(x2)
1328_0_power_Return(x1, x2, x3, x4) → 1328_0_power_Return(x2, x3, x4)
1338_0_power_Return(x1, x2) → 1338_0_power_Return(x2)
Cond_2423_1_main_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_2423_1_main_InvokeMethod1(x1, x3, x4, x6)
1104_0_even_Return(x1, x2, x3) → 1104_0_even_Return
1276_0_even_Return(x1, x2) → 1276_0_even_Return(x2)
1081_0_even_GT(x1, x2, x3) → 1081_0_even_GT(x2, x3)
Cond_1525_0_odd_GT(x1, x2, x3, x4, x5) → Cond_1525_0_odd_GT(x1, x3, x4, x5)
1525_0_odd_GT(x1, x2, x3) → 1525_0_odd_GT(x2, x3)
Cond_1081_0_even_GT(x1, x2, x3, x4) → Cond_1081_0_even_GT(x1, x3, x4)
1302_0_power_NE(x1, x2, x3, x4) → 1302_0_power_NE(x2, x3, x4)
932_0_power_GT(x1, x2, x3, x4) → 932_0_power_GT(x2, x3, x4)
Cond_932_0_power_GT(x1, x2, x3, x4, x5, x6) → Cond_932_0_power_GT(x1, x3, x4, x5, x6)

Filtered duplicate args:

1328_0_power_Return(x1, x2, x3) → 1328_0_power_Return(x1, x3)
991_0_power_Return(x1, x2) → 991_0_power_Return(x2)
932_0_power_GT(x1, x2, x3) → 932_0_power_GT(x1, x3)
1081_0_even_GT(x1, x2) → 1081_0_even_GT(x2)
1525_0_odd_GT(x1, x2) → 1525_0_odd_GT(x2)
Cond_932_0_power_GT(x1, x2, x3, x4, x5) → Cond_932_0_power_GT(x1, x2, x4, x5)
Cond_1081_0_even_GT(x1, x2, x3) → Cond_1081_0_even_GT(x1, x3)
Cond_1525_0_odd_GT(x1, x2, x3, x4) → Cond_1525_0_odd_GT(x1, x3, x4)

Filtered unneeded arguments:

2389_1_main_InvokeMethod(x1, x2, x3, x4, x5) → 2389_1_main_InvokeMethod(x1, x3, x4, x5)
Cond_2423_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_2423_1_main_InvokeMethod(x1, x3, x4, x6)
2526_1_main_InvokeMethod(x1, x2, x3, x4, x5) → 2526_1_main_InvokeMethod(x1, x3, x4, x5)
Cond_2562_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_2562_1_main_InvokeMethod(x1, x3, x4, x6)
Cond_1525_0_odd_GT(x1, x2, x3) → Cond_1525_0_odd_GT(x1, x3)

Filtered all free variables in P and R:

Cond_2423_1_main_InvokeMethod(x1, x2, x3, x4) → Cond_2423_1_main_InvokeMethod(x1, x2, x3)
2526_1_main_InvokeMethod(x1, x2, x3, x4) → 2526_1_main_InvokeMethod(x2, x3)
Cond_2423_1_main_InvokeMethod1(x1, x2, x3, x4) → Cond_2423_1_main_InvokeMethod1(x1, x2, x3)
2562_1_main_InvokeMethod(x1, x2, x3, x4) → 2562_1_main_InvokeMethod(x2, x3)
Cond_2562_1_main_InvokeMethod(x1, x2, x3, x4) → Cond_2562_1_main_InvokeMethod(x1, x2, x3)
2389_1_main_InvokeMethod(x1, x2, x3, x4) → 2389_1_main_InvokeMethod(x2, x3)
Cond_2562_1_main_InvokeMethod1(x1, x2, x3, x4) → Cond_2562_1_main_InvokeMethod1(x1, x2, x3)
Cond_2562_1_main_InvokeMethod2(x1, x2, x3, x4) → Cond_2562_1_main_InvokeMethod2(x1, x2, x3)
Cond_2423_1_main_InvokeMethod2(x1, x2, x3, x4) → Cond_2423_1_main_InvokeMethod2(x1, x2, x3)
Cond_932_0_power_GT(x1, x2, x3, x4) → Cond_932_0_power_GT(x1, x2, x3)
1055_1_power_InvokeMethod(x1, x2, x3, x4) → 1055_1_power_InvokeMethod(x2, x3, x4)
1302_0_power_NE(x1, x2, x3) → 1302_0_power_NE(x1, x3)
Cond_1525_0_odd_GT(x1, x2) → Cond_1525_0_odd_GT(x1)
1640_1_odd_InvokeMethod(x1) → 1640_1_odd_InvokeMethod
1665_0_odd_Return(x1) → 1665_0_odd_Return
2423_1_main_InvokeMethod(x1, x2, x3, x4) → 2423_1_main_InvokeMethod(x2, x3)
1328_0_power_Return(x1, x2) → 1328_0_power_Return(x1)
1276_0_even_Return(x1) → 1276_0_even_Return

Current set of rules:

P rules:
2389_1_main_InvokeMethod(x2, x3) → 2423_1_main_InvokeMethod(java.lang.Object(ARRAY(x3)), x2)
2423_1_main_InvokeMethod(java.lang.Object(ARRAY(x1)), x2) → Cond_2423_1_main_InvokeMethod(&&(<(x2, x1), >(+(x1, 1), 0)), java.lang.Object(ARRAY(x1)), x2)
Cond_2423_1_main_InvokeMethod(TRUE, java.lang.Object(ARRAY(x1)), x2) → 2526_1_main_InvokeMethod(x2, x1)
2423_1_main_InvokeMethod(java.lang.Object(ARRAY(x2)), x3) → Cond_2423_1_main_InvokeMethod1(&&(<(x3, x2), >(+(x2, 1), 0)), java.lang.Object(ARRAY(x2)), x3)
Cond_2423_1_main_InvokeMethod1(TRUE, java.lang.Object(ARRAY(x2)), x3) → 2526_1_main_InvokeMethod(x3, x2)
2526_1_main_InvokeMethod(x2, x3) → 2562_1_main_InvokeMethod(java.lang.Object(ARRAY(x3)), x2)
2562_1_main_InvokeMethod(java.lang.Object(ARRAY(x1)), x2) → Cond_2562_1_main_InvokeMethod(&&(&&(>(+(x2, 1), 0), >(+(x1, 1), 0)), >(x1, +(x2, 1))), java.lang.Object(ARRAY(x1)), x2)
Cond_2562_1_main_InvokeMethod(TRUE, java.lang.Object(ARRAY(x1)), x2) → 2389_1_main_InvokeMethod(+(x2, 1), x1)
2562_1_main_InvokeMethod(java.lang.Object(ARRAY(x2)), x3) → Cond_2562_1_main_InvokeMethod1(&&(&&(>(+(x3, 1), 0), >(+(x2, 1), 0)), >(x2, +(x3, 1))), java.lang.Object(ARRAY(x2)), x3)
Cond_2562_1_main_InvokeMethod1(TRUE, java.lang.Object(ARRAY(x2)), x3) → 2389_1_main_InvokeMethod(+(x3, 1), x2)
2562_1_main_InvokeMethod(java.lang.Object(ARRAY(x2)), x3) → Cond_2562_1_main_InvokeMethod2(&&(&&(>(+(x3, 1), 0), >(+(x2, 1), 0)), >(x2, +(x3, 1))), java.lang.Object(ARRAY(x2)), x3)
Cond_2562_1_main_InvokeMethod2(TRUE, java.lang.Object(ARRAY(x2)), x3) → 2389_1_main_InvokeMethod(+(x3, 1), x2)
2423_1_main_InvokeMethod(java.lang.Object(ARRAY(x2)), x3) → Cond_2423_1_main_InvokeMethod2(&&(<(x3, x2), >(+(x2, 1), 0)), java.lang.Object(ARRAY(x2)), x3)
Cond_2423_1_main_InvokeMethod2(TRUE, java.lang.Object(ARRAY(x2)), x3) → 2526_1_main_InvokeMethod(x3, x2)
R rules:
2389_0_power_Load(x0, x1) → 932_0_power_GT(x0, x1)
2423_0_even_Load(x0) → 1081_0_even_GT(x0)
2526_0_power_Load(x0, x1) → 932_0_power_GT(x0, x1)
2562_0_odd_Load(x0) → 1525_0_odd_GT(x0)
932_0_power_GT(x0, 0) → 949_0_power_Return(x0)
932_0_power_GT(x0, 1) → 991_0_power_Return(x0)
932_0_power_GT(x0, x1) → Cond_932_0_power_GT(>(x1, 1), x0, x1)
Cond_932_0_power_GT(TRUE, x0, x1) → 1055_1_power_InvokeMethod(x0, x1, *(x0, x0))
1055_1_power_InvokeMethod(x2, x3, x0) → 1302_0_power_NE(x2, %(x3, 2))
1302_0_power_NE(x0, 0) → 1328_0_power_Return(x0)
1302_0_power_NE(x0, 1) → 1338_0_power_Return(x1_[0])
1081_0_even_GT(0) → 1104_0_even_Return
1081_0_even_GT(1) → 1151_0_even_Return
1081_0_even_GT(x0) → Cond_1081_0_even_GT(&&(>(x0, 0), !(=(x0, 1))), x0)
Cond_1081_0_even_GT(TRUE, x0) → 1206_1_even_InvokeMethod(1525_0_odd_GT(-(x0, 1)), -(x0, 1))
1206_1_even_InvokeMethod(1604_0_odd_Return, 1) → 1276_0_even_Return
1206_1_even_InvokeMethod(1665_0_odd_Return, x1) → 1276_0_even_Return
1525_0_odd_GT(0) → 1561_0_odd_Return
1525_0_odd_GT(1) → 1604_0_odd_Return
1525_0_odd_GT(x0) → Cond_1525_0_odd_GT(&&(>(x0, 0), !(=(x0, 1))))
Cond_1525_0_odd_GT(TRUE) → 1640_1_odd_InvokeMethod
1640_1_odd_InvokeMethod → 1665_0_odd_Return

Combined rules. Obtained 1 conditional rules for P and 16 conditional rules for R.

P rules:
2389_1_main_InvokeMethod(x0, x1) → 2389_1_main_InvokeMethod(+(x0, 1), x1) | &&(&&(>(x1, -1), >(x1, +(x0, 1))), >(x0, -1))
R rules:
2389_0_power_Load(x0, x1) → 932_0_power_GT(x0, x1)
2526_0_power_Load(x0, x1) → 932_0_power_GT(x0, x1)
2562_0_odd_Load(x0) → 1525_0_odd_GT(x0)
932_0_power_GT(x0, 0) → 949_0_power_Return(x0)
932_0_power_GT(x0, 1) → 991_0_power_Return(x0)
1302_0_power_NE(x0, 0) → 1328_0_power_Return(x0)
1302_0_power_NE(x0, 1) → 1338_0_power_Return(x1_[0])
1206_1_even_InvokeMethod(1604_0_odd_Return, 1) → 1276_0_even_Return
1206_1_even_InvokeMethod(1665_0_odd_Return, x1) → 1276_0_even_Return
1525_0_odd_GT(0) → 1561_0_odd_Return
1525_0_odd_GT(1) → 1604_0_odd_Return
2423_0_even_Load(0) → 1104_0_even_Return
2423_0_even_Load(1) → 1151_0_even_Return
2423_0_even_Load(x0) → 1206_1_even_InvokeMethod(1525_0_odd_GT(-(x0, 1)), -(x0, 1)) | &&(>(x0, 0), !(=(x0, 1)))
932_0_power_GT(x0, x1) → 1302_0_power_NE(x0, %(x1, 2)) | >(x1, 1)
1525_0_odd_GT(x0) → 1665_0_odd_Return | &&(>(x0, 0), !(=(x0, 1)))

Performed bisimulation on rules. Used the following equivalence classes: {[2389_0_power_Load_2, 2526_0_power_Load_2]=2389_0_power_Load_2, [949_0_power_Return_1, 991_0_power_Return_1, 1328_0_power_Return_1, 1338_0_power_Return_1]=949_0_power_Return_1, [1604_0_odd_Return, 1276_0_even_Return, 1665_0_odd_Return, 1561_0_odd_Return, 1104_0_even_Return, 1151_0_even_Return]=1604_0_odd_Return}

Finished conversion. Obtained 2 rules for P and 18 rules for R. System has predefined symbols.

P rules:
2389_1_MAIN_INVOKEMETHOD(x0, x1) → COND_2389_1_MAIN_INVOKEMETHOD(&&(&&(>(x1, -1), >(x1, +(x0, 1))), >(x0, -1)), x0, x1)
COND_2389_1_MAIN_INVOKEMETHOD(TRUE, x0, x1) → 2389_1_MAIN_INVOKEMETHOD(+(x0, 1), x1)
R rules:
2389_0_power_Load(x0, x1) → 932_0_power_GT(x0, x1)
2562_0_odd_Load(x0) → 1525_0_odd_GT(x0)
932_0_power_GT(x0, 0) → 949_0_power_Return(x0)
932_0_power_GT(x0, 1) → 949_0_power_Return(x0)
1302_0_power_NE(x0, 0) → 949_0_power_Return(x0)
1302_0_power_NE(x0, 1) → 949_0_power_Return(x1_[0])
1206_1_even_InvokeMethod(1604_0_odd_Return, 1) → 1604_0_odd_Return
1206_1_even_InvokeMethod(1604_0_odd_Return, x1) → 1604_0_odd_Return
1525_0_odd_GT(0) → 1604_0_odd_Return
1525_0_odd_GT(1) → 1604_0_odd_Return
2423_0_even_Load(0) → 1604_0_odd_Return
2423_0_even_Load(1) → 1604_0_odd_Return
2423_0_even_Load(x0) → Cond_2423_0_even_Load(&&(>(x0, 0), !(=(x0, 1))), x0)
Cond_2423_0_even_Load(TRUE, x0) → 1206_1_even_InvokeMethod(1525_0_odd_GT(-(x0, 1)), -(x0, 1))
932_0_power_GT(x0, x1) → Cond_932_0_power_GT(>(x1, 1), x0, x1)
Cond_932_0_power_GT(TRUE, x0, x1) → 1302_0_power_NE(x0, %(x1, 2))
1525_0_odd_GT(x0) → Cond_1525_0_odd_GT(&&(>(x0, 0), !(=(x0, 1))), x0)
Cond_1525_0_odd_GT(TRUE, x0) → 1604_0_odd_Return

(21) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

The ITRS R consists of the following rules:
2389_0_power_Load(x0, x1) → 932_0_power_GT(x0, x1)
2562_0_odd_Load(x0) → 1525_0_odd_GT(x0)
932_0_power_GT(x0, 0) → 949_0_power_Return(x0)
932_0_power_GT(x0, 1) → 949_0_power_Return(x0)
1302_0_power_NE(x0, 0) → 949_0_power_Return(x0)
1302_0_power_NE(x0, 1) → 949_0_power_Return(x1_[0])
1206_1_even_InvokeMethod(1604_0_odd_Return, 1) → 1604_0_odd_Return
1206_1_even_InvokeMethod(1604_0_odd_Return, x1) → 1604_0_odd_Return
1525_0_odd_GT(0) → 1604_0_odd_Return
1525_0_odd_GT(1) → 1604_0_odd_Return
2423_0_even_Load(0) → 1604_0_odd_Return
2423_0_even_Load(1) → 1604_0_odd_Return
2423_0_even_Load(x0) → Cond_2423_0_even_Load(x0 > 0 && !(x0 = 1), x0)
Cond_2423_0_even_Load(TRUE, x0) → 1206_1_even_InvokeMethod(1525_0_odd_GT(x0 - 1), x0 - 1)
932_0_power_GT(x0, x1) → Cond_932_0_power_GT(x1 > 1, x0, x1)
Cond_932_0_power_GT(TRUE, x0, x1) → 1302_0_power_NE(x0, x1 % 2)
1525_0_odd_GT(x0) → Cond_1525_0_odd_GT(x0 > 0 && !(x0 = 1), x0)
Cond_1525_0_odd_GT(TRUE, x0) → 1604_0_odd_Return

The integer pair graph contains the following rules and edges:
(0): 2389_1_MAIN_INVOKEMETHOD(x0[0], x1[0]) → COND_2389_1_MAIN_INVOKEMETHOD(x1[0] > -1 && x1[0] > x0[0] + 1 && x0[0] > -1, x0[0], x1[0])
(1): COND_2389_1_MAIN_INVOKEMETHOD(TRUE, x0[1], x1[1]) → 2389_1_MAIN_INVOKEMETHOD(x0[1] + 1, x1[1])

(0) -> (1), if (x1[0] > -1 && x1[0] > x0[0] + 1 && x0[0] > -1 ∧x0[0] →^* x0[1]∧x1[0] →^* x1[1])

(1) -> (0), if (x0[1] + 1 →^* x0[0]∧x1[1] →^* x1[0])

The set Q consists of the following terms:
2389_0_power_Load(x0, x1)
2562_0_odd_Load(x0)
1302_0_power_NE(x0, 0)
1302_0_power_NE(x0, 1)
1206_1_even_InvokeMethod(1604_0_odd_Return, x0)
2423_0_even_Load(x0)
Cond_2423_0_even_Load(TRUE, x0)
932_0_power_GT(x0, x1)
Cond_932_0_power_GT(TRUE, x0, x1)
1525_0_odd_GT(x0)
Cond_1525_0_odd_GT(TRUE, x0)

(22) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@4468dbbe Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 2389_1_MAIN_INVOKEMETHOD(x0, x1) → COND_2389_1_MAIN_INVOKEMETHOD(&&(&&(>(x1, -1), >(x1, +(x0, 1))), >(x0, -1)), x0, x1) the following chains were created:

We consider the chain 2389_1_MAIN_INVOKEMETHOD(x0[0], x1[0]) → COND_2389_1_MAIN_INVOKEMETHOD(&&(&&(>(x1[0], -1), >(x1[0], +(x0[0], 1))), >(x0[0], -1)), x0[0], x1[0]), COND_2389_1_MAIN_INVOKEMETHOD(TRUE, x0[1], x1[1]) → 2389_1_MAIN_INVOKEMETHOD(+(x0[1], 1), x1[1]) which results in the following constraint:
(1)    (&&(&&(>(x1[0], -1), >(x1[0], +(x0[0], 1))), >(x0[0], -1))=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 2389_1_MAIN_INVOKEMETHOD(x0[0], x1[0])≥NonInfC∧2389_1_MAIN_INVOKEMETHOD(x0[0], x1[0])≥COND_2389_1_MAIN_INVOKEMETHOD(&&(&&(>(x1[0], -1), >(x1[0], +(x0[0], 1))), >(x0[0], -1)), x0[0], x1[0])∧(U^Increasing(COND_2389_1_MAIN_INVOKEMETHOD(&&(&&(>(x1[0], -1), >(x1[0], +(x0[0], 1))), >(x0[0], -1)), x0[0], x1[0])), ≥))

We simplified constraint (1) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (>(x0[0], -1)=TRUE∧>(x1[0], -1)=TRUE∧>(x1[0], +(x0[0], 1))=TRUE ⇒ 2389_1_MAIN_INVOKEMETHOD(x0[0], x1[0])≥NonInfC∧2389_1_MAIN_INVOKEMETHOD(x0[0], x1[0])≥COND_2389_1_MAIN_INVOKEMETHOD(&&(&&(>(x1[0], -1), >(x1[0], +(x0[0], 1))), >(x0[0], -1)), x0[0], x1[0])∧(U^Increasing(COND_2389_1_MAIN_INVOKEMETHOD(&&(&&(>(x1[0], -1), >(x1[0], +(x0[0], 1))), >(x0[0], -1)), x0[0], x1[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x1[0] + [-2] + [-1]x0[0] ≥ 0 ⇒ (U^Increasing(COND_2389_1_MAIN_INVOKEMETHOD(&&(&&(>(x1[0], -1), >(x1[0], +(x0[0], 1))), >(x0[0], -1)), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_32] + [(2)bni_32]x1[0] + [(-1)bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x1[0] + [-2] + [-1]x0[0] ≥ 0 ⇒ (U^Increasing(COND_2389_1_MAIN_INVOKEMETHOD(&&(&&(>(x1[0], -1), >(x1[0], +(x0[0], 1))), >(x0[0], -1)), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_32] + [(2)bni_32]x1[0] + [(-1)bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x1[0] + [-2] + [-1]x0[0] ≥ 0 ⇒ (U^Increasing(COND_2389_1_MAIN_INVOKEMETHOD(&&(&&(>(x1[0], -1), >(x1[0], +(x0[0], 1))), >(x0[0], -1)), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_32] + [(2)bni_32]x1[0] + [(-1)bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0∧[2] + x0[0] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2389_1_MAIN_INVOKEMETHOD(&&(&&(>(x1[0], -1), >(x1[0], +(x0[0], 1))), >(x0[0], -1)), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_32 + (4)bni_32] + [bni_32]x0[0] + [(2)bni_32]x1[0] ≥ 0∧[(-1)bso_33] ≥ 0)

For Pair COND_2389_1_MAIN_INVOKEMETHOD(TRUE, x0, x1) → 2389_1_MAIN_INVOKEMETHOD(+(x0, 1), x1) the following chains were created:

We consider the chain COND_2389_1_MAIN_INVOKEMETHOD(TRUE, x0[1], x1[1]) → 2389_1_MAIN_INVOKEMETHOD(+(x0[1], 1), x1[1]) which results in the following constraint:
(7)    (COND_2389_1_MAIN_INVOKEMETHOD(TRUE, x0[1], x1[1])≥NonInfC∧COND_2389_1_MAIN_INVOKEMETHOD(TRUE, x0[1], x1[1])≥2389_1_MAIN_INVOKEMETHOD(+(x0[1], 1), x1[1])∧(U^Increasing(2389_1_MAIN_INVOKEMETHOD(+(x0[1], 1), x1[1])), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(2389_1_MAIN_INVOKEMETHOD(+(x0[1], 1), x1[1])), ≥)∧[bni_34] = 0∧[1 + (-1)bso_35] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(2389_1_MAIN_INVOKEMETHOD(+(x0[1], 1), x1[1])), ≥)∧[bni_34] = 0∧[1 + (-1)bso_35] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(2389_1_MAIN_INVOKEMETHOD(+(x0[1], 1), x1[1])), ≥)∧[bni_34] = 0∧[1 + (-1)bso_35] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(2389_1_MAIN_INVOKEMETHOD(+(x0[1], 1), x1[1])), ≥)∧[bni_34] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_35] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

2389_1_MAIN_INVOKEMETHOD(x0, x1) → COND_2389_1_MAIN_INVOKEMETHOD(&&(&&(>(x1, -1), >(x1, +(x0, 1))), >(x0, -1)), x0, x1)
- (x0[0] ≥ 0∧[2] + x0[0] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2389_1_MAIN_INVOKEMETHOD(&&(&&(>(x1[0], -1), >(x1[0], +(x0[0], 1))), >(x0[0], -1)), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_32 + (4)bni_32] + [bni_32]x0[0] + [(2)bni_32]x1[0] ≥ 0∧[(-1)bso_33] ≥ 0)
COND_2389_1_MAIN_INVOKEMETHOD(TRUE, x0, x1) → 2389_1_MAIN_INVOKEMETHOD(+(x0, 1), x1)
- ((U^Increasing(2389_1_MAIN_INVOKEMETHOD(+(x0[1], 1), x1[1])), ≥)∧[bni_34] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_35] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(2389_0_power_Load(x₁, x₂)) = [-1]
POL(932_0_power_GT(x₁, x₂)) = [-1] + [-1]x₂
POL(2562_0_odd_Load(x₁)) = [-1]
POL(1525_0_odd_GT(x₁)) = [-1] + [-1]x₁
POL(0) = 0
POL(949_0_power_Return(x₁)) = [-1]
POL(1) = [1]
POL(1302_0_power_NE(x₁, x₂)) = [-1] + [-1]x₂
POL(1206_1_even_InvokeMethod(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(1604_0_odd_Return) = [-1]
POL(2423_0_even_Load(x₁)) = [-1] + [-1]x₁
POL(Cond_2423_0_even_Load(x₁, x₂)) = [-1] + [-1]x₂
POL(&&(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(!(x₁)) = [-1]
POL(=(x₁, x₂)) = [-1]
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(Cond_932_0_power_GT(x₁, x₂, x₃)) = [-1] + [-1]x₃
POL(2) = [2]
POL(Cond_1525_0_odd_GT(x₁, x₂)) = [-1] + [-1]x₂
POL(2389_1_MAIN_INVOKEMETHOD(x₁, x₂)) = [2]x₂ + [-1]x₁
POL(COND_2389_1_MAIN_INVOKEMETHOD(x₁, x₂, x₃)) = [2]x₃ + [-1]x₂
POL(-1) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂

The following pairs are in P_>:

COND_2389_1_MAIN_INVOKEMETHOD(TRUE, x0[1], x1[1]) → 2389_1_MAIN_INVOKEMETHOD(+(x0[1], 1), x1[1])

The following pairs are in P_bound:

2389_1_MAIN_INVOKEMETHOD(x0[0], x1[0]) → COND_2389_1_MAIN_INVOKEMETHOD(&&(&&(>(x1[0], -1), >(x1[0], +(x0[0], 1))), >(x0[0], -1)), x0[0], x1[0])

The following pairs are in P_≥:

2389_1_MAIN_INVOKEMETHOD(x0[0], x1[0]) → COND_2389_1_MAIN_INVOKEMETHOD(&&(&&(>(x1[0], -1), >(x1[0], +(x0[0], 1))), >(x0[0], -1)), x0[0], x1[0])

There are no usable rules.

(23) Complex Obligation (AND)

(24) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

The ITRS R consists of the following rules:
2389_0_power_Load(x0, x1) → 932_0_power_GT(x0, x1)
2562_0_odd_Load(x0) → 1525_0_odd_GT(x0)
932_0_power_GT(x0, 0) → 949_0_power_Return(x0)
932_0_power_GT(x0, 1) → 949_0_power_Return(x0)
1302_0_power_NE(x0, 0) → 949_0_power_Return(x0)
1302_0_power_NE(x0, 1) → 949_0_power_Return(x1_[0])
1206_1_even_InvokeMethod(1604_0_odd_Return, 1) → 1604_0_odd_Return
1206_1_even_InvokeMethod(1604_0_odd_Return, x1) → 1604_0_odd_Return
1525_0_odd_GT(0) → 1604_0_odd_Return
1525_0_odd_GT(1) → 1604_0_odd_Return
2423_0_even_Load(0) → 1604_0_odd_Return
2423_0_even_Load(1) → 1604_0_odd_Return
2423_0_even_Load(x0) → Cond_2423_0_even_Load(x0 > 0 && !(x0 = 1), x0)
Cond_2423_0_even_Load(TRUE, x0) → 1206_1_even_InvokeMethod(1525_0_odd_GT(x0 - 1), x0 - 1)
932_0_power_GT(x0, x1) → Cond_932_0_power_GT(x1 > 1, x0, x1)
Cond_932_0_power_GT(TRUE, x0, x1) → 1302_0_power_NE(x0, x1 % 2)
1525_0_odd_GT(x0) → Cond_1525_0_odd_GT(x0 > 0 && !(x0 = 1), x0)
Cond_1525_0_odd_GT(TRUE, x0) → 1604_0_odd_Return

The integer pair graph contains the following rules and edges:
(0): 2389_1_MAIN_INVOKEMETHOD(x0[0], x1[0]) → COND_2389_1_MAIN_INVOKEMETHOD(x1[0] > -1 && x1[0] > x0[0] + 1 && x0[0] > -1, x0[0], x1[0])

The set Q consists of the following terms:
2389_0_power_Load(x0, x1)
2562_0_odd_Load(x0)
1302_0_power_NE(x0, 0)
1302_0_power_NE(x0, 1)
1206_1_even_InvokeMethod(1604_0_odd_Return, x0)
2423_0_even_Load(x0)
Cond_2423_0_even_Load(TRUE, x0)
932_0_power_GT(x0, x1)
Cond_932_0_power_GT(TRUE, x0, x1)
1525_0_odd_GT(x0)
Cond_1525_0_odd_GT(TRUE, x0)

(25) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(26) TRUE

(27) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

The ITRS R consists of the following rules:
2389_0_power_Load(x0, x1) → 932_0_power_GT(x0, x1)
2562_0_odd_Load(x0) → 1525_0_odd_GT(x0)
932_0_power_GT(x0, 0) → 949_0_power_Return(x0)
932_0_power_GT(x0, 1) → 949_0_power_Return(x0)
1302_0_power_NE(x0, 0) → 949_0_power_Return(x0)
1302_0_power_NE(x0, 1) → 949_0_power_Return(x1_[0])
1206_1_even_InvokeMethod(1604_0_odd_Return, 1) → 1604_0_odd_Return
1206_1_even_InvokeMethod(1604_0_odd_Return, x1) → 1604_0_odd_Return
1525_0_odd_GT(0) → 1604_0_odd_Return
1525_0_odd_GT(1) → 1604_0_odd_Return
2423_0_even_Load(0) → 1604_0_odd_Return
2423_0_even_Load(1) → 1604_0_odd_Return
2423_0_even_Load(x0) → Cond_2423_0_even_Load(x0 > 0 && !(x0 = 1), x0)
Cond_2423_0_even_Load(TRUE, x0) → 1206_1_even_InvokeMethod(1525_0_odd_GT(x0 - 1), x0 - 1)
932_0_power_GT(x0, x1) → Cond_932_0_power_GT(x1 > 1, x0, x1)
Cond_932_0_power_GT(TRUE, x0, x1) → 1302_0_power_NE(x0, x1 % 2)
1525_0_odd_GT(x0) → Cond_1525_0_odd_GT(x0 > 0 && !(x0 = 1), x0)
Cond_1525_0_odd_GT(TRUE, x0) → 1604_0_odd_Return

The integer pair graph contains the following rules and edges:
(1): COND_2389_1_MAIN_INVOKEMETHOD(TRUE, x0[1], x1[1]) → 2389_1_MAIN_INVOKEMETHOD(x0[1] + 1, x1[1])

The set Q consists of the following terms:
2389_0_power_Load(x0, x1)
2562_0_odd_Load(x0)
1302_0_power_NE(x0, 0)
1302_0_power_NE(x0, 1)
1206_1_even_InvokeMethod(1604_0_odd_Return, x0)
2423_0_even_Load(x0)
Cond_2423_0_even_Load(TRUE, x0)
932_0_power_GT(x0, x1)
Cond_932_0_power_GT(TRUE, x0, x1)
1525_0_odd_GT(x0)
Cond_1525_0_odd_GT(TRUE, x0)

(28) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPNonInfProof (SOUND transformation)

(9) Obligation:

(10) IDependencyGraphProof (EQUIVALENT transformation)

(11) TRUE

(12) Obligation:

(13) SCCToIDPv1Proof (SOUND transformation)

(14) Obligation:

(15) IDPNonInfProof (SOUND transformation)

(16) Obligation:

(17) IDependencyGraphProof (EQUIVALENT transformation)

(18) TRUE

(19) Obligation:

(20) SCCToIDPv1Proof (SOUND transformation)

(21) Obligation:

(22) IDPNonInfProof (SOUND transformation)

(23) Complex Obligation (AND)

(24) Obligation:

(25) IDependencyGraphProof (EQUIVALENT transformation)

(26) TRUE

(27) Obligation:

(28) IDependencyGraphProof (EQUIVALENT transformation)

(29) TRUE